Ignore:
Timestamp:
Dec 3, 2012, 4:15:03 PM (7 years ago)
Author:
sacerdot
Message:

Generic stuff moved to infrastructure.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/infrastructure.ma

    r2514 r2522  
    55
    66coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     7
     8lemma dep_bool_match_elim :
     9∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop.
     10∀c1,c2.
     11(∀prf : Q true.P (c1 prf)) →
     12(∀prf : Q false.P (c2 prf)) →
     13∀prf : Q b.
     14P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf).
     15* // qed.
    716
    817definition defined : ∀T:Type[0]. option T → bool ≝
Note: See TracChangeset for help on using the changeset viewer.