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

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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 2.1 KB
Line 
1include "Maybe.ma".
2include "Nat.ma".
3
4ninductive List (A: Type[0]): Type[0] ≝
5  Empty: List A
6| Cons: A → List A → List A.
7
8notation "hvbox(hd break :: tl)"
9  right associative with precedence 47
10  for @{ 'Cons $hd $tl }.
11
12interpretation "Empty" 'Empty = (Empty ?).
13interpretation "Cons" 'Cons = (Cons ?).
14 
15notation "[ list0 x sep ; ]"
16  non associative with precedence 90
17  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
18 
19nlet 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   
25nlet 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   
31notation "hvbox(l break @ r)"
32  right associative with precedence 47
33  for @{ 'append $l $r }.
34 
35interpretation "Append" 'append = (append ?).
36 
37nlet 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   
44nlet 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   
51nlet 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   
58nlet rec null (A: Type[0]) (l: List A) on l ≝
59  match l with
60    [ Empty ⇒ True
61    | Cons hd tl ⇒ False
62    ].
63   
64nlet 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   
70ndefinition 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   
78ndefinition 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     
86nlet 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    ].
Note: See TracBrowser for help on using the repository browser.