LIST
The data type of
def List-ctor (A: U) := maybe-rec A U π (Ξ» (a : A), π)
def List (A: U) := W (x : Maybe A), List-ctor A x
In type theory
Introduction
You can create zero list with
def nil (A: U) : List A
def cons (A: U) (x : A) (xs: List A) : List A
Elimination
Induction principle allows you to prove general predicate on
def List-ind (A: U) (C: List A -> U)
(z: C (nil A)) (s: Ξ (x: A) (xs: List A), C xs -> C (cons A x xs))
: Ξ (n: List A), C n
def List-rec (A: U) (C : U) (z : C) (s : A β List A β C β C) : List A β C
def List-iter (A: U) (C : U) (z : C) (s : A β C β C) : List A β C
def List-case (A: U) (C : U) (z : C) (s : A β C) : List A β C