Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	array → nat
. + .	nat-basic2	f	nat × nat → nat
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	array	f	array × nat → elem
. [ . ]	array	f	array × nat × elem → array
. ∈ .	array-copy	p	elem × array
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
c	elem	v	elem
cmp	array-copy	p	array × elem × nat × nat
cmp	array-copy	p	array × nat × array × nat × nat
copy	array-copy	f	array × nat × array × nat × nat → array
elem	elem	s
fill	array-copy	f	array × elem × nat × nat → array
fill	array-copy	f	array × elem → array
id○	array-copy	p	array × array × nat
idrange	array-copy	p	array × nat × nat
m	nat-basic1	v	nat
m0	array-copy	v	nat
mkarray	array	f	nat → array
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
rev	array-copy	f	array × nat → array
rev	array-copy	f	array → array
subarray	array-copy	f	array × nat × nat → array