Changeset 411
 Timestamp:
 Dec 13, 2010, 5:11:00 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/IOMonad.ma
r366 r411 177 177 178 178 179 (* TODO: is there a way to prove this without extensionality?179 (* Is there a way to prove this without extensionality? *) 180 180 181 nlemma bind_assoc_r: ∀A,B,C,e,f,g. 182 bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g). 183 #A B C e f g; nelim e; 184 ##[ #fn args k IH; nwhd in ⊢ (???%); 185 nnormalize; 186 *) 181 nlemma bind_assoc_r: ∀O,I,A,B,C,e,f,g. 182 ∀ext:(∀T1,T2:Type.∀f,f':T1 → T2.(∀x.f x = f' x) → f = f'). 183 bindIO O I B C (bindIO O I A B e f) g = bindIO O I A C e (λx.bindIO O I B C (f x) g). 184 #O I A B C e f g ext; nelim e; 185 ##[ #o k IH; nwhd in ⊢ (??%%); napply eq_f; 186 napply ext; napply IH; 187 ## #v; napply refl; 188 ## napply refl; 189 ##] nqed. 190 187 191 188 192 nlemma extract_subset_pair_io: ∀O,I,A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→IO O I C. ∀R:C→Prop.
Note: See TracChangeset
for help on using the changeset viewer.