Changeset 1351 for src/common


Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (8 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1316 r1351  
    9292notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    9393  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     94
     95definition 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
     102notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
     103interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
    94104
    95105(*
Note: See TracChangeset for help on using the changeset viewer.