source: src/ERTL/ERTLToLTL.ma @ 753

Last change on this file since 753 was 753, checked in by mulligan, 9 years ago

Work from today.

File size: 538 bytes
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3 
4axiom translate_ERTL_func:
5  ∀globals: list Identifier.
6    list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
7 
8definition translate: ∀e: ERTLProgram. LTLProgram (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_LTLProgram (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.