add splitKind to HaskKind

[coq-hetmet.git] / src / HaskKinds.v

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 1452045..b5cc2ff 100644 (file)
--- 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.
+