-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 coreVarToWeakVar : CoreVar -> CoreVarToWeakVarResult. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
+Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars".