Changeset 1608 for src/common
- Timestamp:
- Dec 14, 2011, 2:30:39 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Errors.ma
r1601 r1608 91 91 (* Dependent pair version. *) 92 92 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 93 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp${ident v} ${ident p} ⇒ ${e'} ]) }.93 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }. 94 94 95 95 lemma Prod_extensionality:
Note: See TracChangeset
for help on using the changeset viewer.