Changeset 1647 for src/common/IOMonad.ma


Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1640 r1647  
    2424
    2525definition IOMonad ≝ λO,I.
    26   MakeMonad (mk_MonadDefinition
     26  MakeMonadProps
    2727  (* the monad *)
    2828  (IO O I)
     
    3131  (* bind *)
    3232  (bindIO O I)
    33   ???). / by /
    34 [(* bind_bind *)
     33  ???. / by /
     34[(* bind_ret *)
     35 #X#m elim m normalize // #o#f#Hi @interact_proper //
     36|(* bind_bind *)
    3537 #X#Y#Z#m#f#g elim m normalize [2,3://]
    3638 (* Interact *)
    3739  #o#f #Hi @interact_proper //
    38 |(* bind_ret *)
    39  #X#m elim m normalize // #o#f#Hi @interact_proper //
    4040]
    4141qed.
     
    4646
    4747unification hint 0 ≔ O, I, T;
    48   N ≟ IOMonad O I, M ≟ m_def N
     48  N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M
    4949(*******************************************) ⊢
    50   IO O I T ≡ monad M T
     50  IO O I T ≡ monad M' T
    5151.
    5252
     
    177177  P_io O I ? P (bindIO O I A B e f).
    178178#I #O #A #B #P' #P #e elim e;
    179 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     179[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    180180| #v #f #He #H @H @He
    181181| //;
     
    187187  P_io O I ? P (bindIO2 O I A B C e f).
    188188#I #O #A #B #C #P' #P #e elim e;
    189 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     189[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    190190| #v cases v; #v1 #v2 #f #He #H @H @He
    191191| //;
     
    213213#I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
    214214[ *;
    215 | #e'' cases e''; #a #b #Pab #H normalize; /2/;
     215| #e'' cases e''; #a #b #Pab #H normalize; /2 by _/;
    216216] qed.
    217217*)
Note: See TracChangeset for help on using the changeset viewer.