Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	list-data	f	List[A] → Nat
. '	list	f	A → List[A]
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	A × List[A] → List[A]
. + .	list	f	List[A] × List[A] → List[A]
. + .	list	f	List[A] × A → List[A]
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	A × A → List[A]
. - .	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
. ∈ .	list	p	'A × List('A)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. foldLeft ( . )	list	f	List[A] × B × (B × A → B) → B
. head	list-data	pf	List[A] → A with λ x. x ≠ []
. map ( . )	list	f	List[A] × (A → B) → List[B]
. 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	v	A
b	list	v	B
bx	list	v	List[B]
f	list	v	A → B
n	list	v	Nat
x	list	v	List[A]
y	list	v	List[A]
z	list	v	List[A]