source: src/LTL/LTLToLIN.ma @ 723

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

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

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