Changeset 1351 for src/common/Errors.ma
 Timestamp:
 Oct 11, 2011, 12:24:33 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1316 r1351 92 92 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 93 93 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }. 94 95 definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝ 96 λA,B,C,P,e,f. 97 match e with 98 [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ] 99  Error msg ⇒ Error ? msg 100 ]. 101 102 notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}. 103 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f). 94 104 95 105 (*
Note: See TracChangeset
for help on using the changeset viewer.