[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
# .	datastream	f	datastream → natinf
# .	dataarray	f	dataarray → nat
# .	datastream	f	datalist → nat
. '	datastream	f	data → datalist
. + .	nat-basic2	f	nat × nat → nat
. + .	datastream	f	datastream × datastream → datastream
. + .	dataarray	f	dataarray × dataarray → dataarray
. + .	datastream	f	data × datastream → datastream
. + .	datastream	f	data × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	datastream	f	datalist × datalist → datalist
. + .	datastream	f	datalist × data → datalist
. + .	datastream	f	data × data → datalist
. ++ .	datastream	f	datalist × data → datalist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	datastream	f	datalist × nat → datalist
. -1l .	datastream	f	datalist × data → datalist
. -l .	datastream	f	datalist × data → datalist
. .ar	datastream-conv	f	datastream → dataarray
. .butlast	datastream	f	datalist → datalist
. .f	datastream	f	datastream → nat → data
. .first	datastream	f	datalist → data
. .l	datastream	f	datastream → datalist
. .last	datastream	f	datalist → data
. .n	nat-inf-basic	f	natinf → nat
. .rest	datastream	f	datalist → datalist
. < .	nat-inf	p	natinf × natinf
. < .	datastream	p	datalist × datalist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	dataarray	f	dataarray × nat → data
. [ . ]	dataarray	f	dataarray × nat × data → dataarray
. [ . ]	datastream	f	datastream × nat × data → datastream
. [ . ]	datastream	f	datalist × nat → data
. [ . ]	datastream	f	datastream × nat → data
. [ . ]	datastream	f	datalist × nat × data → datalist
. ∈ .	datastream	p	data × datalist
. ∈ .	dataarray	p	data × dataarray
. ≤ .	datastream	p	datastream × datastream
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	datastream	p	datalist × datalist
. ⊒ .	datastream	p	datalist × datalist
. from .	datastream	f	datastream × nat → datastream
. from .	datastream	f	(nat → data) × nat → nat → data
. from .	datastream	f	datalist × nat → datalist
. to .	datastream	f	datastream × nat → datastream
. to .	datastream	f	(nat → data) × nat → datalist
. to .	datastream	f	datalist × nat → datalist
. to∞ .	datastream	f	datastream × natinf → datastream
[]	datastream	c	datalist
[]	datastream	c	datastream
σ	datastream	v	datastream
σ⊥	datastream-conv	c	datastream
σ1	datastream	v	datastream
σ2	datastream	v	datastream
∞	nat-inf-basic	c	natinf
⌜ . ⌝	datastream	f	datalist → datastream
⌜ . ⌝	datastream	f	(nat → data) → datastream
⌜ . ⌝	nat-inf-basic	f	nat → natinf
⌜ . ⌝	datastream-conv	f	dataarray → datastream
ar	dataarray	v	dataarray
ar0	dataarray	v	dataarray
ar1	dataarray	v	dataarray
ar2	dataarray	v	dataarray
butlastn	datastream	f	nat × datalist → datalist
cmp	dataarray	p	dataarray × data × nat × nat
cmp	dataarray	p	dataarray × nat × dataarray × nat × nat
copy	dataarray	f	dataarray × nat × dataarray × nat × nat → dataarray
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
dataarray	dataarray	s
datalist	datastream	s
datastream	datastream	s
disj	datastream	p	datalist × datalist
dups	datastream	p	datalist
dx	datastream	v	datalist
dx0	datastream	v	datalist
dx1	datastream	v	datalist
dx10	datastream	v	datalist
dx2	datastream	v	datalist
dx3	datastream	v	datalist
dx4	datastream	v	datalist
dx5	datastream	v	datalist
dx6	datastream	v	datalist
dx7	datastream	v	datalist
dx8	datastream	v	datalist
dx9	datastream	v	datalist
empty	dataarray	c	data
fill	dataarray	f	dataarray × data × nat × nat → dataarray
fill	dataarray	f	dataarray × data → dataarray
fillfirst	datastream	f	nat × data × datalist → datalist
finp	datastream	p	datastream
firstn	datastream	f	nat × datalist → datalist
frome	datastream	f	datalist × data → datalist
hd	datastream	f	datastream → data
id○	dataarray	p	dataarray × dataarray × nat
idrange	dataarray	p	dataarray × nat × nat
lastn	datastream	f	nat × datalist → datalist
m	nat-basic1	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
min	nat-inf	f	natinf × natinf → natinf
mkarray	dataarray	f	nat → dataarray
mkemparray	dataarray	f	nat → dataarray
mklist	datastream	f	data × nat → datalist
mkzarray	dataarray	f	nat → dataarray
n	nat-basic1	v	nat
n∞	nat-inf-basic	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
natinf	nat-inf-basic	s
nf	datastream	v	nat → data
nf0	datastream	v	nat → data
pos	datastream	f	data × datalist → nat
range=	dataarray	p	dataarray × nat × dataarray × nat × nat
resize	dataarray	f	dataarray × nat → dataarray
restn	datastream	f	nat × datalist → datalist
rev	dataarray	f	dataarray → dataarray
rev	datastream	f	datalist → datalist
rev	dataarray	f	dataarray × nat → dataarray
rmdup	datastream	f	datalist → datalist
splice	dataarray	f	dataarray × nat × dataarray × nat × nat → dataarray
subarray	dataarray	f	dataarray × nat × nat → dataarray
sublist	datastream	f	nat × nat × datalist → datalist
tl	datastream	f	datastream → datastream
zero	dataarray	c	data