Changeset 1920 for src/common
 Timestamp:
 May 8, 2012, 11:16:18 AM (8 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1882 r1920 207 207 ] qed. 208 208 209 lemma intsize_eq_elim_false : ∀A,sz,sz',P,p,f,d. 210 sz ≠ sz' → 211 intsize_eq_elim A sz sz' P p f d = d. 212 #A * * // #P #p #f #d * #H cases (H (refl ??)) 213 qed. 209 214 210 215 (* A type for the integers that appear in the semantics. *) 
src/common/IOMonad.ma
r1882 r1920 218 218 ] qed. 219 219 *) 220 221 (* Inversion when injecting errors into IO monad. *) 222 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. 223 (∀a. e = OK A a → f a = OK B v → P v) → 224 (match e »= f with [ OK v ⇒ Value … v  Error m ⇒ Wrong … m ] = Value O I B v → P v). 225 #O #I #A #B * 226 [ #a #f #v #P #H #E @H [ @a  @refl  normalize in E; cases (f a) in E ⊢ %; 227 [ #v' #E normalize in E; destruct @refl  #m #E normalize in E; destruct ] ] 228  #m #f #v #P #H #E whd in E:(??%?); destruct 229 ] qed. 230 231 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. 232 (∀a. e = Value ??? a → f a = Value ??? v → P v) → 233 (bindIO O I A B e f = Value ??? v → P v). 234 #O #I #A #B * 235 [ #o #k #f #v #P #H #E whd in E:(??%?); destruct 236  #a #f #v #P #H #E @H [ @a  @refl  @E ] 237  #m #f #v #P #H #E whd in E:(??%?); destruct 238 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.