Ignore:
Timestamp:
Sep 8, 2011, 4:04:07 PM (9 years ago)
Author:
campbell
Message:

Clight cast removal (NB: quite different from the prototype).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r891 r1198  
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    9292λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
     93
     94definition type_eq : type → type → bool ≝
     95λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
     96
Note: See TracChangeset for help on using the changeset viewer.