Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (8 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r891 r1250  
    721721| #m #H @(False_ind … H)
    722722] qed.
     723
     724(* Stuff about Sigma types *)
     725definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
     726 λA,P,c. match c with [ dp w _ ⇒ w ].
     727coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
Note: See TracChangeset for help on using the changeset viewer.