From 4fec54f1f2cdb072d03928f94f1d45f58755bc13 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 15:10:13 -0700 Subject: [PATCH] add splitKind to HaskKind --- src/HaskKinds.v | 7 +++++++ 1 file changed, 7 insertions(+) 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. + -- 1.7.10.4