Changeset 1598 for src/common


Ignore:
Timestamp:
Dec 12, 2011, 5:53:36 PM (9 years ago)
Author:
mulligan
Message:

changes over the last couple of days

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1355 r1598  
    6060definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
    6161  match f with
    62   [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
     62  [ OK v ⇒ g (fst … v) (snd … v)
    6363  | Error msg => Error ? msg
    6464  ].
     
    6666definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
    6767  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)
    6969  | Error msg => Error ? msg
    7070  ].
     
    9393  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
    9494
     95lemma Prod_extensionality:
     96  ∀a, b: Type[0].
     97  ∀p: a × b.
     98    p = 〈fst … p, snd … p〉.
     99  #a #b #p //
     100qed.
     101
    95102definition 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 ≝
    96103λA,B,C,P,e,f.
    97104  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') ? ]
    99106  | Error msg ⇒ Error ? msg
    100107  ].
     108  <(Prod_extensionality A B v')
     109  assumption
     110qed.
    101111
    102112notation > "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.