X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=85d6f24e38664e8bc48ca175fa53bb7bd3325ad5;hb=bb960df7c29c851ca9d13f2d0c8f351ac24045ca;hp=e721de905f7c3be750fd0ce7fd2665edeae29fc5;hpb=14a87dd821c4194382f29eef2d59fe932d4124c1;p=coq-hetmet.git

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index e721de9..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 *)
@@ -385,13 +364,35 @@ Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 Fixpoint update_ξ
   `{EQD_VV:EqDecidable VV}{Γ}
    (ξ:VV -> LeveledHaskType Γ ★)
-   (vt:list (VV * LeveledHaskType Γ ★))
+   (lev:HaskLevel Γ)
+   (vt:list (VV * HaskType Γ ★))
    : VV -> LeveledHaskType Γ ★ :=
   match vt with
     | nil => ξ
-    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
   end.
 
+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+  not (In v (map (@fst _ _) varstypes)) ->
+  (update_ξ ξ lev varstypes) v = ξ v.
+  intros.
+  induction varstypes.
+  reflexivity.
+  simpl.
+  destruct a.
+  destruct (eqd_dec v0 v).
+  subst.
+  simpl in  H.
+  assert False. 
+  apply H.
+  auto.
+  inversion H0.
+  apply IHvarstypes.
+  unfold not; intros.
+  apply H.
+  simpl.
+  auto.
+  Defined.
 
 
 (***************************************************************************************************)