Changeset 985 for src/common


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (8 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r961 r985  
    599599definition bool_to_Prop ≝
    600600 λb. match b with [ true ⇒ True | false ⇒ False ].
     601
     602coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    601603
    602604(* dpm: should go to standard library *)
Note: See TracChangeset for help on using the changeset viewer.