blob: 8e9ba5ffda44fbdc76b8f71ef18d7817c4396b2c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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)
)
|
