source: src/ERTL/ERTLToLTL.ma @ 757

Last change on this file since 757 was 757, checked in by mulligan, 10 years ago

Lots more fixing to get both front and backends using same conventions and types.

File size: 529 bytes
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3 
4axiom translate_ERTL_func:
5  ∀globals: list ident.
6    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
7 
8definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
9  λp.
10    let globals ≝ map ? ? \fst (ertl_pr_vars p) in
11    let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in
12      mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p).
13    # H1
14    @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)
Note: See TracBrowser for help on using the repository browser.