Changeset 2796 for src/utilities/extralib.ma
- Timestamp:
- Mar 7, 2013, 12:10:42 PM (8 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.