Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	array → nat
. + .	nat-basic	f	nat × nat → nat
. + .	array-listops	f	elem × array → array
. +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
. .first	array-listops	pf	array → elem with λ ar. ar ≠ []
. .rest	array-listops	pf	array → array with λ ar. ar ≠ []
. < .	nat-basic	p	nat × nat
. < .	array-listops	p	array × array
. > .	nat	p	nat × nat
. [ . ]	array	pf	array × nat → elem with λ ar, n. n < # ar
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
[]	array-listops	c	array
a	array-listops	v	elem
ar	array-listops	v	array
array	array	s
cmp	array-copy	p	array × elem
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
copy	array-copy	pf	array × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
elem	elem	s
fill	array-copy	f	array × elem → array
fill	array-copy	pf	array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
id○	array-copy	p	array × array × nat
id○	array-copy	p	array × array × nat × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
mkarray	array	f	nat → array
n	array-listops	v	nat
nat	nat-basic	s
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar