Changeset 2533


Ignore:
Timestamp:
Dec 5, 2012, 7:20:23 PM (7 years ago)
Author:
campbell
Message:

Some fall out from removing floats.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2510 r2533  
    267267
    268268(* 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/
     269definition 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  ].
     275destruct %
    272276qed.
    273277
     
    469473  P t1 v1 →
    470474  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
     476whd in ⊢ (??%? → ?); cases (typ_eq t1 t2)
     477[ #E destruct #E whd in E:(??%?); destruct //
     478| #NE #E normalize in E; destruct
     479] qed.
    475480
    476481lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop.
  • src/common/Animation.ma

    r2176 r2533  
    1212match io_in_typ o return λt. res (eventval_type t) with
    1313[ 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) ]
    1514| ASTptr ⇒ Error ? (msg IllTypedEvent)
    1615].
Note: See TracChangeset for help on using the changeset viewer.