git @ Cat's Eye Technologies Dipple / master
Show that, for lists, Nil is the unit for append. Chris Pressey 19 days ago
1 changed file(s) with 26 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
0 module ListJazz
1
2 // It's possible to use lowercase greek letters for type variables in an inductive type definition:
3
4 type list α =
5 | Nil : list α
6 | Cons : head:α -> tail:list α -> list α
7
8 // But, as of this writing, not as parameters to a function (implicit or otherwise).
9
10 let rec length #a (l:list a) =
11 match l with
12 | Nil -> 0
13 | Cons head tail -> 1 + length tail
14
15 let rec append #a (la:list a) (lb:list a) : result:list a { length result = length la + length lb } =
16 match la with
17 | Nil -> lb
18 | Cons head tail -> Cons head (append tail lb)
19
20 let rec append_has_nil_as_unit #a (l:list a)
21 : Lemma ((append Nil l == l) /\ (append l Nil == l))
22 =
23 match l with
24 | Nil -> ()
25 | Cons head tail -> append_has_nil_as_unit tail