Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	list-data	f	List[A] → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	A × List[A] → List[A]
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('A) × List('A)
. > .	nat	p	Nat × Nat
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. head	list-data	pf	List[A] → A with λ x. x ≠ []
. tail	list-data	pf	List[A] → List[A] with λ x. x ≠ []
[]	list-data	c	List[A]
List	list-data	s
Nat	nat-basic	s
a	list-data	v	A
head	list-data	v	A
n	list-data	v	Nat
tail	list-data	v	List[A]
x	list-data	v	List[A]
y	list-data	v	List[A]
z	list-data	v	List[A]