...

[bitonic-mengthesis.git] / demo.ka

diff --git a/demo.ka b/demo.ka
index 8e9ba5ffda44fbdc76b8f71ef18d7817c4396b2c..60ebdeaa5463c0966cfba8c1fd890c2a6eefca30 100644 (file)
--- a/demo.ka
+++ b/demo.ka
@@ -11,31 +11,12 @@ 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)
+    {| h1 |}
+    {| h2 |}
 )