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

Generic stuff moved to infrastructure.

Location:
Papers/polymorphic-variants-2012
Files:
2 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 ≝
  • Papers/polymorphic-variants-2012/variants.ma

    r2520 r2522  
    3838whd in match (is_in ???); >H //
    3939qed.
    40 
    41 lemma dep_bool_match_elim :
    42 ∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop.
    43 ∀c1,c2.
    44 (∀prf : Q true.P (c1 prf)) →
    45 (∀prf : Q false.P (c2 prf)) →
    46 ∀prf : Q b.
    47 P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf).
    48 * // qed.
    4940
    5041lemma Q_of_Q_ok':
Note: See TracChangeset for help on using the changeset viewer.