Ignore:
Timestamp:
Mar 4, 2011, 6:20:28 PM (9 years ago)
Author:
campbell
Message:

Switch to more conservative definitions in preparation for review.
(Efficient mul/div via Z, sort out some disambiguation problems that have
appeared.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r583 r638  
    344344#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    345345
    346 let rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
     346let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    347347match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    348348[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     
    421421λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
    422422
    423 let rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     423let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
    424424match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
    425425[ Kstop ⇒ ?
Note: See TracChangeset for help on using the changeset viewer.