Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r2453 r2529  
    211211  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
    212212
     213let rec m_fold (M : Monad)
     214  X Y (f : X → Y → M Y) (l : list X) (init : Y) on l : M Y ≝
     215match 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
     222lemma 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]
     230qed.
     231
    213232unification hint 0 ≔ M, X, Y, Z, m, f ;
    214233  P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢
Note: See TracChangeset for help on using the changeset viewer.