Changeset 1598 for src/common
 Timestamp:
 Dec 12, 2011, 5:53:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1355 r1598 60 60 definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C. 61 61 match f with 62 [ OK v ⇒ match v with [ pair x y ⇒ g x y ]62 [ OK v ⇒ g (fst … v) (snd … v) 63 63  Error msg => Error ? msg 64 64 ]. … … 66 66 definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D. 67 67 match f with 68 [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]68 [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v) 69 69  Error msg => Error ? msg 70 70 ]. … … 93 93 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }. 94 94 95 lemma Prod_extensionality: 96 ∀a, b: Type[0]. 97 ∀p: a × b. 98 p = 〈fst … p, snd … p〉. 99 #a #b #p // 100 qed. 101 95 102 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 103 λA,B,C,P,e,f. 97 104 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]105 [ OK v ⇒ match v with [ dp v' p ⇒ f (fst … v') (snd … v') ? ] 99 106  Error msg ⇒ Error ? msg 100 107 ]. 108 <(Prod_extensionality A B v') 109 assumption 110 qed. 101 111 102 112 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'})}.
Note: See TracChangeset
for help on using the changeset viewer.