source: src/ERTL/ERTLToLTL.ma @ 752

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

Fixed error in BitVectorTrieSet? file.

File size: 411 bytes
Line 
1include "ERTL/ERTL.ma".
2 
3axiom translate_func:
4  ∀globals: list Identifier.
5    list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
6 
7definition translate: ERTLProgram → LTLProgram ≝
8  λp.
9    let globals ≝ map ? ? \fst (ERTL_Pr_Vars e) in
10    let ltl_pr_var ≝ ERTL_Pr_Vars e in
11    let ltl_pr_funcs ≝ map ? ? (translate_func globals) (ERTL_Pr_Funcs e) in
Note: See TracBrowser for help on using the repository browser.