X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;fp=src%2FHaskKinds.v;h=b5cc2ffdef0bffe584c48a2a2dce81938ccb43c8;hp=1452045e63f730a656e02d3f5be22758982d021e;hb=4fec54f1f2cdb072d03928f94f1d45f58755bc13;hpb=48bc98e014fd0c21ca75017bf689e8e6e80f54e3

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 1452045..b5cc2ff 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -50,3 +50,10 @@ Instance KindEqDecidable : EqDecidable Kind.
     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
   Defined.
 
+(* splits a kind into a list of arguments and a result *)
+Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
+  match k with
+    | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
+    | _     => (nil, k)
+  end.
+