Ignore:
Timestamp:
Sep 23, 2011, 3:04:20 PM (9 years ago)
Author:
mulligan
Message:

commit for csc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1250 r1260  
    721721| #m #H @(False_ind … H)
    722722] qed.
    723 
    724 (* Stuff about Sigma types *)
    725 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    726  λA,P,c. match c with [ dp w _ ⇒ w ].
    727 coercion 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.