...

1 files changed, 2 insertions, 21 deletions

diff --git a/demo.ka b/demo.ka
index 8e9ba5f..60ebdea 100644
--- a/demo.ka
+++ b/demo.ka
@@ -12,30 +12,11 @@ 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)
+    {| h1 |}
+    {| h2 |}
 )