// SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
// For more information, please refer to <https://unlicense.org/>
// SPDX-License-Identifier: Unlicense
module ListJazz
// It's possible to use lowercase greek letters for type variables in an inductive type definition:
type list α =
| Nil : list α
| Cons : head:α -> tail:list α -> list α
// But, as of this writing, not as parameters to a function (implicit or otherwise).
let rec length #a (l:list a) =
match l with
| Nil -> 0
| Cons head tail -> 1 + length tail
let rec append #a (la:list a) (lb:list a) : result:list a { length result = length la + length lb } =
match la with
| Nil -> lb
| Cons head tail -> Cons head (append tail lb)
let rec append_has_nil_as_unit #a (l:list a)
: Lemma ((append Nil l == l) /\ (append l Nil == l))
=
match l with
| Nil -> ()
| Cons head tail -> append_has_nil_as_unit tail