From aec3c690756a1918a9b1756e930a920a7514ff37 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:14:04 -0700 Subject: [PATCH] remove unnecessary instance from HaskStrongTypes --- src/HaskStrongTypes.v | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index f8493b4..85d6f24 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -53,27 +53,6 @@ Inductive DataCon : TyCon -> Type := Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon. (*Opaque DataCon.*) -Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool. - intros. - destruct dc1. - destruct dc2. - exact (if eqd_dec cdc cdc0 then true else false). - Defined. - -Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2). - -Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc). - intros. - apply Build_EqDecidable. - intros. - set (trust_compare_datacons _ v1 v2) as x. - set (compare_datacons tc v1 v2) as y. - assert (y=compare_datacons tc v1 v2). reflexivity. - destruct y; rewrite <- H in x. - left; auto. - right; auto. - Defined. - Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc). (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) -- 1.7.10.4