Changeset 1949 for src/utilities/monad.ma
 Timestamp:
 May 15, 2012, 5:51:25 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r1882 r1949 152 152 153 153 include "hints_declaration.ma". 154 154 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". 155 155 unification hint 0 ≔ M, X; 156 156 M' ≟ smax_def M, S ≟ setoid_of_monad M X … … 226 226 mk_SetoidMonadProps (mk_Monad monad m_return m_bind). 227 227 228 include "basics/russell.ma". 229 228 230 record MonadPred (M : Monad) : Type[1] ≝ 229 231 { m_pred :> ∀X.pred_transformer X (monad M X) 232 ; mp_inject : ∀X,P.(Σm.m_pred X P m) → monad M (Σx.P x) 230 233 ; mp_return : ∀X,P,x.P x → m_pred X P (return x) 231 234 ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m → … … 233 236 m_pred ? Pout (m_bind … m f) 234 237 ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X) 235 }. 238 ; mp_inject_eq : ∀X,P,m.pi1 ?? m = ! x ← mp_inject X P m ; return pi1 … x 239 }. 240 241 coercion coerc_mp_inject : ∀M.∀MP:MonadPred M. 242 ∀X,P.∀m : Σm.m_pred ? MP X P m.monad M (Σx.P x) ≝ 243 mp_inject on _m : Sig (monad ??) (λm.m_pred ???? m) to monad ? (Sig ? (λx.? x)). 244 245 lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → monad M Y. 246 ! x ← mp_inject M MP X P m ; f (pi1 … x) = ! x ← pi1 … m ; f x. 247 #M#MP#X#P#Y#m#f >mp_inject_eq >m_bind_bind @m_bind_ext_eq #x >m_return_bind % qed. 236 248 237 249 record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ … … 242 254 ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y) 243 255 }. 256 257
Note: See TracChangeset
for help on using the changeset viewer.