Changeset 638 for Deliverables/D3.1/Csemantics/Cexec.ma
 Timestamp:
 Mar 4, 2011, 6:20:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Cexec.ma
r583 r638 344 344 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 345 345 346 let rec type_eq_dec (t1,t2:type) : (t1 = t2) +(t1 ≠ t2) ≝346 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ 347 347 match t1 return λt'. (t' = t2) + (t' ≠ t2) with 348 348 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??)  _ ⇒ inr ?? (nmk ? (λH.?)) ] … … 421 421 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p  inr _ ⇒ Error ? ]. 422 422 423 let rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝423 let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝ 424 424 match k return λk'.(is_call_cont k') + (¬is_call_cont k') with 425 425 [ Kstop ⇒ ?
Note: See TracChangeset
for help on using the changeset viewer.