source: Deliverables/D4.1/Matita/List.ma @ 229

Last change on this file since 229 was 229, checked in by mulligan, 10 years ago

More changes.

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