Changeset 714 for src/LIN


Ignore:
Timestamp:
Mar 29, 2011, 12:24:45 PM (9 years ago)
Author:
mulligan
Message:

Work on translation from LTL to LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r699 r714  
    77alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    88alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    9 
    10 (* dpm: should go to standard library *)
    11 let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    12                (g: list Identifier) on g: Prop ≝
    13   match g with
    14   [ nil ⇒ False
    15   | cons hd tl ⇒
    16       bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
    17   ].
    189
    1910inductive LINStatement (globals: list Identifier): Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.