source: src/LTL/LTLToLIN.ma @ 722

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

Committing changes from today. Several files do not typecheck.

File size: 342 bytes
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3
4definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝
5  λglobals: list Identifier.
6  λs: LTLStatement globals.
7    match s with
8    [ LIN_St_Return ⇒ LIN_St_Return ? globals
9    | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it
10    ].
Note: See TracBrowser for help on using the repository browser.