From 27d8348b35af1e7d5b2bc92e299f075f7b8de8e9 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Sun, 23 Jun 2013 15:07:05 +0100
Subject: [PATCH] ...

---
 demo.ka | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 demo.ka

diff --git a/demo.ka b/demo.ka
new file mode 100644
index 0000000..8e9ba5f
--- /dev/null
+++ b/demo.ka
@@ -0,0 +1,41 @@
+data Empty : * ⇒ {}
+
+absurd [A : *] [x : Empty] : A ⇒ (
+  Empty-Elim x (λ _ ⇒ A)
+)
+
+record Unit : * ⇒ tt {}
+
+data Nat : * ⇒ { zero : Nat | suc : Nat → Nat }
+
+data List : [A : *] → * ⇒
+  { nil : List A | cons : A → List A → List A }
+
+nonEmpty [A : *] [l : List A] : * ⇒ (
+   {| h1 |}
+)
+
+nonEmpty [A : *] [l : List A] : * ⇒ (
+  List-Elim l (λ _ ⇒ *) {|h1|} {|h2|}
+)
+
+nonEmpty [A : *] [l : List A] : * ⇒ (
+  List-Elim l (λ _ ⇒ *) Empty (λ _ _ _ ⇒ Unit)
+)
+
+head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
+  List-Elim l (λ l ⇒ nonEmpty A l → A)
+    {|h1|} {|h2|}
+)
+
+head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
+  List-Elim l (λ l ⇒ nonEmpty A l → A)
+   (λ p ⇒ {|h1 p|})
+   (λ x l pl pxl ⇒ {|h2 x l pl pxl|})
+)
+
+head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
+  List-Elim l (λ l ⇒ nonEmpty A l → A)
+    (λ p ⇒ absurd A p)
+    (λ x l pl pxl ⇒ x)
+)
-- 
2.30.2