Changeset 2529 for src/utilities/monad.ma
 Timestamp:
 Dec 4, 2012, 6:16:25 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r2453 r2529 211 211 λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y. 212 212 213 let rec m_fold (M : Monad) 214 X Y (f : X → Y → M Y) (l : list X) (init : Y) on l : M Y ≝ 215 match l with 216 [ nil ⇒ return init 217  cons hd tl ⇒ 218 ! y ← f hd init ; 219 m_fold M X Y f tl y 220 ]. 221 222 lemma m_fold_append : ∀M : MonadProps.∀X,Y,f,l1,l2,init. 223 m_fold M X Y f (l1@l2) init = 224 ! y ← m_fold … f l1 init ; 225 m_fold … f l2 y. 226 #M #X #Y #f #l1 elim l1 l1 227 [ #l2 #init >m_return_bind % 228  #hd #tl #IH #l2 #init >m_bind_bind @m_bind_ext_eq #y @IH 229 ] 230 qed. 231 213 232 unification hint 0 ≔ M, X, Y, Z, m, f ; 214 233 P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢
Note: See TracChangeset
for help on using the changeset viewer.