[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	dataarray	f	dataarray → nat
. + .	dataarray	f	dataarray × dataarray → dataarray
. + .	nat-basic	f	nat × nat → nat
. +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
. > .	nat	p	nat × nat
. [ . ]	dataarray	pf	dataarray × nat × data → dataarray with λ ar0, n, d. n < # ar0
. [ . ]	dataarray	pf	dataarray × nat → data with λ ar0, n. n < # ar0
. ∈ .	dataarray	p	data × dataarray
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
ar	dataarray	v	dataarray
ar0	dataarray	v	dataarray
ar1	dataarray	v	dataarray
ar2	dataarray	v	dataarray
cmp	dataarray	pp	dataarray × data × nat × nat with λ ar0, d, m, n. m + n ≤ # ar0
cmp	dataarray	pp	dataarray × nat × dataarray × nat × nat with λ ar1, m, ar2, m0, n. m + n ≤ # ar1 ∧ m0 + n ≤ # ar2
copy	dataarray	pf	dataarray × nat × dataarray × nat × nat → dataarray with λ ar1, m, ar2, m0, n. m + n ≤ # ar1 ∧ m0 + n ≤ # ar2
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
dataarray	dataarray	s
empty	dataarray	c	data
fill	dataarray	pf	dataarray × data × nat × nat → dataarray with λ ar0, d, n, m. n + m ≤ # ar0
fill	dataarray	f	dataarray × data → dataarray
id○	dataarray	p	dataarray × dataarray × nat
idrange	dataarray	pp	dataarray × nat × nat with λ ar0, m, n. m + n ≤ # ar0
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkarray	dataarray	f	nat → dataarray
mkemparray	dataarray	f	nat → dataarray
mkzarray	dataarray	f	nat → dataarray
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
range=	dataarray	p	dataarray × nat × dataarray × nat × nat
resize	dataarray	f	dataarray × nat → dataarray
rev	dataarray	pf	dataarray × nat → dataarray with λ ar0, n. n ≤ # ar0
rev	dataarray	f	dataarray → dataarray
splice	dataarray	f	dataarray × nat × dataarray × nat × nat → dataarray
subarray	dataarray	pf	dataarray × nat × nat → dataarray with λ ar0, m, n. m + n ≤ # ar0
zero	dataarray	c	data