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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r1640 r1647 24 24 25 25 definition IOMonad ≝ λO,I. 26 MakeMonad (mk_MonadDefinition26 MakeMonadProps 27 27 (* the monad *) 28 28 (IO O I) … … 31 31 (* bind *) 32 32 (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 *) 35 37 #X#Y#Z#m#f#g elim m normalize [2,3://] 36 38 (* Interact *) 37 39 #o#f #Hi @interact_proper // 38 (* bind_ret *)39 #X#m elim m normalize // #o#f#Hi @interact_proper //40 40 ] 41 41 qed. … … 46 46 47 47 unification hint 0 ≔ O, I, T; 48 N ≟ IOMonad O I, M ≟ m _def N48 N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M 49 49 (*******************************************) ⊢ 50 IO O I T ≡ monad M T50 IO O I T ≡ monad M' T 51 51 . 52 52 … … 177 177 P_io O I ? P (bindIO O I A B e f). 178 178 #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 /; 180 180  #v #f #He #H @H @He 181 181  //; … … 187 187 P_io O I ? P (bindIO2 O I A B C e f). 188 188 #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 /; 190 190  #v cases v; #v1 #v2 #f #He #H @H @He 191 191  //; … … 213 213 #I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize; 214 214 [ *; 215  #e'' cases e''; #a #b #Pab #H normalize; /2 /;215  #e'' cases e''; #a #b #Pab #H normalize; /2 by _/; 216 216 ] qed. 217 217 *)
Note: See TracChangeset
for help on using the changeset viewer.