From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Thu, 1 Sep 2011 04:35:17 +0000 (-0700)
Subject: add examples of first-order (kappa calculus) terms at level-1
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=7523e5094db5e00224ba034b00aa243e69211c9f

add examples of first-order (kappa calculus) terms at level-1
---

diff --git a/examples/KappaDemo.hs b/examples/KappaDemo.hs
new file mode 100644
index 0000000..f052012
--- /dev/null
+++ b/examples/KappaDemo.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types #-}
+module Demo (demo, demo2) where
+
+demo  z   = <{ \y -> ~~z }>
+
+demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
+demo2 x y = <{ ~~x ~~y }>
+
+demo3 x y z q = <{ ~~q (~~x ~~y ~~z) }>
+
+
+
diff --git a/examples/Makefile b/examples/Makefile
index f880d81..09e4b9c 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -5,6 +5,7 @@ open:
 	open .build/test.pdf
 
 #sanity += BiGArrow.hs
+sanity += KappaDemo.hs
 sanity += CircuitExample.hs
 sanity += CommandSyntaxExample.hs
 sanity += DotProduct.hs