1 | include "Maybe.ma". |
---|
2 | include "Nat.ma". |
---|
3 | |
---|
4 | ninductive List (A: Type[0]): Type[0] ≝ |
---|
5 | Empty: List A |
---|
6 | | Cons: A → List A → List A. |
---|
7 | |
---|
8 | notation "hvbox(hd break :: tl)" |
---|
9 | right associative with precedence 47 |
---|
10 | for @{ 'Cons $hd $tl }. |
---|
11 | |
---|
12 | interpretation "Empty" 'Empty = (Empty ?). |
---|
13 | interpretation "Cons" 'Cons = (Cons ?). |
---|
14 | |
---|
15 | notation "[ list0 x sep ; ]" |
---|
16 | non associative with precedence 90 |
---|
17 | for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }. |
---|
18 | |
---|
19 | nlet rec length (A: Type[0]) (l: List A) on l ≝ |
---|
20 | match l with |
---|
21 | [ Empty ⇒ Z |
---|
22 | | Cons hd tl ⇒ S (length A tl) |
---|
23 | ]. |
---|
24 | |
---|
25 | nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝ |
---|
26 | match l with |
---|
27 | [ Empty ⇒ m |
---|
28 | | Cons hd tl ⇒ hd :: (append A tl l) |
---|
29 | ]. |
---|
30 | |
---|
31 | notation "hvbox(l break @ r)" |
---|
32 | right associative with precedence 47 |
---|
33 | for @{ 'append $l $r }. |
---|
34 | |
---|
35 | interpretation "Append" 'append = (append ?). |
---|
36 | |
---|
37 | nlet rec fold_right (A: Type[0]) (B: Type[0]) |
---|
38 | (f: A → B → B) (x: B) (l: List A) on l ≝ |
---|
39 | match l with |
---|
40 | [ Empty ⇒ x |
---|
41 | | Cons hd tl ⇒ f hd (fold_right A B f x tl) |
---|
42 | ]. |
---|
43 | |
---|
44 | nlet rec fold_left (A: Type[0]) (B: Type[0]) |
---|
45 | (f: A → B → A) (x: A) (l: List B) on l ≝ |
---|
46 | match l with |
---|
47 | [ Empty ⇒ x |
---|
48 | | Cons hd tl ⇒ f (fold_left A B f x tl) hd |
---|
49 | ]. |
---|
50 | |
---|
51 | nlet rec map (A: Type[0]) (B: Type[0]) |
---|
52 | (f: A → B) (l: List A) on l ≝ |
---|
53 | match l with |
---|
54 | [ Empty ⇒ Empty B |
---|
55 | | Cons hd tl ⇒ f hd :: map A B f tl |
---|
56 | ]. |
---|
57 | |
---|
58 | nlet rec null (A: Type[0]) (l: List A) on l ≝ |
---|
59 | match l with |
---|
60 | [ Empty ⇒ True |
---|
61 | | Cons hd tl ⇒ False |
---|
62 | ]. |
---|
63 | |
---|
64 | nlet rec reverse (A: Type[0]) (l: List A) on l ≝ |
---|
65 | match l with |
---|
66 | [ Empty ⇒ Empty A |
---|
67 | | Cons hd tl ⇒ reverse A tl @ (Cons A hd (Empty A)) |
---|
68 | ]. |
---|
69 | |
---|
70 | ndefinition head ≝ |
---|
71 | λA: Type[0]. |
---|
72 | λl: List A. |
---|
73 | match l with |
---|
74 | [ Empty ⇒ Nothing A |
---|
75 | | Cons hd tl ⇒ Just A hd |
---|
76 | ]. |
---|
77 | |
---|
78 | ndefinition tail ≝ |
---|
79 | λA: Type[0]. |
---|
80 | λl: List A. |
---|
81 | match l with |
---|
82 | [ Empty ⇒ Nothing (List A) |
---|
83 | | Cons hd tl ⇒ Just (List A) tl |
---|
84 | ]. |
---|
85 | |
---|
86 | nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝ |
---|
87 | match n with |
---|
88 | [ Z ⇒ Empty A |
---|
89 | | S o ⇒ a :: (replicate A o a) |
---|
90 | ]. |
---|