Changeset 714 for src/common


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

Work on translation from LTL to LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r699 r714  
    77definition Identifier ≝ Byte.
    88definition Immediate ≝ nat.
     9
     10definition bool_to_Prop ≝
     11 λb. match b with [ true ⇒ True | false ⇒ False ].
     12
     13(* dpm: should go to standard library *)
     14let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
     15               (g: list Identifier) on g: Prop ≝
     16  match g with
     17  [ nil ⇒ False
     18  | cons hd tl ⇒
     19      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
     20  ].
    921
    1022inductive Compare: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.