Changeset 1647 for src/common/Errors.ma
 Timestamp:
 Jan 17, 2012, 1:13:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1640 r1647 49 49 (*Implicit Arguments Error [A].*) 50 50 51 definition Res : Monad ≝ MakeMonad (mk_MonadDefinition51 definition Res ≝ MakeMonadProps 52 52 (* the monad *) 53 53 res … … 56 56 (* bind *) 57 57 (λX,Y,m,f. match m with [ OK x ⇒ f x  Error msg ⇒ Error ? msg]) 58 ??? ).58 ???. 59 59 // 60 [(* bind_bind *) 60 [(* bind_ret *) 61 #X*normalize // 62 (* bind_bind *) 61 63 #X#Y#Z*normalize // 62 (* bind_ret *)63 #X*normalize //64 64 ] 65 65 qed. … … 67 67 include "hints_declaration.ma". 68 68 unification hint 0 ≔ X; 69 M ≟ m_def Res 69 N ≟ max_def Res, M ≟ m_def N 70 70 (**) ⊢ 71 71 res X ≡ monad M X … … 96 96 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*) 97 97 98 lemma res_bind_inversion:98 lemma bind_inversion: 99 99 ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B. 100 100 (f »= g = return y) → … … 250 250 ] (refl ? f). 251 251 252 notation > "vbox(' !' ident v 'as' ident E ← e; break e')" with precedence 40for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.252 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 253 253 254 254 definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. … … 258 258 ] (refl ? f). 259 259 260 notation > "vbox(' !' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.260 notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}. 261 261 262 262 definition res_to_opt : ∀A:Type[0]. res A → option A ≝ 263 263 λA.λv. match v with [ Error _ ⇒ None ?  OK v ⇒ Some … v]. 264 264 265 (* aliases for backward compatibility *) 266 definition bind ≝ m_bind Res. 267 definition bind2 ≝ m_bind2 Res. 268 definition bind3 ≝ m_bind3 Res. 269 definition mmap ≝ m_mmap Res. 270 definition mmap_sigma ≝ m_mmap_sigma Res.
Note: See TracChangeset
for help on using the changeset viewer.