 Timestamp:
 Dec 5, 2012, 7:20:23 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2510 r2533 267 267 268 268 (* same gig for AST typs *) 269 definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). 270 * [ #sz1 #sg1  ] 271 * try /2 by Error/ 269 definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2) ≝ 270 λty1,ty2,P,p. 271 match typ_eq ty1 ty2 with 272 [ inl E ⇒ OK ? (p⌈P ty1 ↦ P ty2⌉) 273  inr _ ⇒ Error ? (msg TypeMismatch) 274 ]. 275 destruct % 272 276 qed. 273 277 … … 469 473 P t1 v1 → 470 474 P t2 v2. 471 * [ #sz #sg  ] 472 * [ 1,3: * * ] 473 #P #v1 #v2 #E whd in E:(??%?); destruct 474 qed. 475 #t1 #t2 #P #v1 #v2 476 whd in ⊢ (??%? → ?); cases (typ_eq t1 t2) 477 [ #E destruct #E whd in E:(??%?); destruct // 478  #NE #E normalize in E; destruct 479 ] qed. 475 480 476 481 lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop. 
src/common/Animation.ma
r2176 r2533 12 12 match io_in_typ o return λt. res (eventval_type t) with 13 13 [ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent))  _ ⇒ Error ? (msg IllTypedEvent) ] 14  ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f  _ ⇒ Error ? (msg IllTypedEvent) ]15 14  ASTptr ⇒ Error ? (msg IllTypedEvent) 16 15 ].
Note: See TracChangeset
for help on using the changeset viewer.