Changeset 2796 for src/utilities
 Timestamp:
 Mar 7, 2013, 12:10:42 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r2309 r2796 204 204 for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒ 205 205 λ${ident E}.$s ] (refl ? $t) }. 206 207 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 208 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 209 210 interpretation "exists in Type[1]" 'exists_Type1 x = (ex_Type1 ? x). 211 212 notation < "hvbox(∃\sub 1 ident i : ty break . p)" 213 right associative with precedence 20 214 for @{'exists_Type1 (\lambda ${ident i} : $ty. $p) }. 215 216 notation > "\exists[1] list1 ident x sep , opt (: T). term 19 Px" 217 with precedence 20 218 for ${ default 219 @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}:$T.$acc)} } } 220 @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}.$acc)} } } 221 }.
Note: See TracChangeset
for help on using the changeset viewer.