-Definition weakTypeToCoreType (wt:WeakType) :=
- weakTypeToCoreType' (normalizeWeakType wt).
-
-Definition compare_weakTypes (w1 w2:WeakType) :=
- if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
- then true
- else false.
-
-(*
-Instance EqDecidableWeakType : EqDecidable WeakType.
- apply Build_EqDecidable.
- intros.
- set (compare_weakTypes_axiom v1 v2) as x.
- set (compare_weakTypes v1 v2) as y.
- assert (y=compare_weakTypes v1 v2). reflexivity.
- destruct y; rewrite <- H in x.
- left; auto.
- right; auto.
- Defined.
-*)
-