From 72d3380355a80135c91e77736f1ebb6ca4f43923 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 15:10:33 -0700 Subject: [PATCH] revise tyFunKind to use splitKind --- src/HaskWeakVars.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index f174563..44e267d 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -48,9 +48,11 @@ Definition tyConTyVars (tc:CoreTyCon) := Opaque tyConTyVars. Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). -Variable tyFunResultKind : CoreTyCon -> Kind. Extract Inlined Constant tyFunResultKind => "tyFunResultKind". + +Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)". + Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) := - ((map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc)) , (tyFunResultKind tc)). + splitKind (rawTyFunKind tc). (* (* EqDecidable instances for all of the above *) -- 1.7.10.4