diff options
Diffstat (limited to 'demo.ka')
-rw-r--r-- | demo.ka | 23 |
1 files changed, 2 insertions, 21 deletions
@@ -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 |} ) |