Expand description
List.
Structs§
- FConcat
- List concatenation.
- FCons
- A non-empty list.
- FLen
- Length of list.
- FList
- A list.
- FNil
- An empty list.
- Head
head(a).- Tail
tail(a).
Functions§
- concat_
cons (cons{x}(a, b) : list(x)) ⋀ (c : list(x)) => concat{x}(cons{x}(a, b), c) == cons{x}(a, concat{x}(b, c)).- concat_
nil (nil{x} : list(x)) ⋀ (a : list(x)) => concat{x}(nil{x}, a) == a.- concat_
ty (a : type(0)) => (concat{a} : (list(a), list(a)) -> list(a)).- cons_ty
a : type(0) => cons{a} : (a, list(a)) -> list(a).- head_ty
(a : list(b)) ⋀ ¬(a == nil{b}) => head(a) : b.- len_
cons cons{x}(a, b) : list(a) => len{x}(cons{x}(a, b)) == succ(len{x}(b)).- len_nil
nil{a} : list(a) => len(nil{a}) == 0.- len_ty
(a : type(0)) => (len{a} : list(a) -> nat).- list_
def a : list(b) => (a == nil{b}) ⋁ (a == cons{b}(head(a), tail(a))).- list_
exists ∃ nil{a} : list(a) { x } ⋀ ∃ cons{a}(b, c) : list(a) { x } => x.- list_ty
(a : type(0)) => (list : a -> type(0)).- nil_ty
(a : type(0)) => (nil{a} : list(a)).- norm1_
concat_ len concat{x}[len{x}] == add.- tail_ty
(a : list(b)) ⋀ ¬(a == nil{b}) => tail(a) : list(b).