Changeset 752


Ignore:
Timestamp:
Apr 14, 2011, 2:23:30 PM (9 years ago)
Author:
mulligan
Message:

Fixed error in BitVectorTrieSet? file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r745 r752  
    11include "ERTL/ERTL.ma".
    22 
     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 TracChangeset for help on using the changeset viewer.