Changeset 2533 for src/Clight/toCminor.ma
 Timestamp:
 Dec 5, 2012, 7:20:23 PM (9 years ago)
 File:

 1 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.
Note: See TracChangeset
for help on using the changeset viewer.