X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=demo.ka;h=60ebdeaa5463c0966cfba8c1fd890c2a6eefca30;hb=6731f090d5edb85f628501e5dcc513e542fce325;hp=8e9ba5ffda44fbdc76b8f71ef18d7817c4396b2c;hpb=ec1119dffc5801526058a816d498b58e3c8f9e7f;p=bitonic-mengthesis.git

diff --git a/demo.ka b/demo.ka
index 8e9ba5f..60ebdea 100644
--- 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 |}
 )