-(* EqDecidable instances for all of the above *)
-Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
- apply Build_EqDecidable.
- intros.
- destruct v1 as [cv1 t1a t1b].
- destruct v2 as [cv2 t2a t2b].
- destruct (eqd_dec cv1 cv2); subst.
- destruct (eqd_dec t1a t2a); subst.
- destruct (eqd_dec t1b t2b); subst.
- left; auto.
- right; intro; apply n; inversion H; subst; auto.
- right; intro; apply n; inversion H; subst; auto.
- right; intro; apply n; inversion H; subst; auto.
- Defined.
+Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
+Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars".
+Definition tyConTyVars (tc:CoreTyCon) :=
+ filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
+ Opaque tyConTyVars.
+Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
+
+Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".