[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
# .	datastream	f	datalist → nat
. '	datastream	f	data → datalist
. + .	nat-basic2	f	nat × nat → nat
. + .	datastream	f	datastream × datastream → datastream
. + .	datastream	f	data × datalist → datalist
. + .	datastream	f	data × datastream → datastream
. + .	datastream	f	datalist × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	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
. .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
. [ . ]	datastream	f	datalist × nat → data
. [ . ]	datastream	f	datalist × nat × data → datalist
. [ . ]	datastream	f	datastream × nat × data → datastream
. [ . ]	datastream	f	datastream × nat → data
. ∈ .	datastream	p	data × datalist
. ≤ .	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
σ1	datastream	v	datastream
σ2	datastream	v	datastream
∞	nat-inf-basic	c	natinf
⌜ . ⌝	nat-inf-basic	f	nat → natinf
⌜ . ⌝	datastream	f	datalist → datastream
⌜ . ⌝	datastream	f	(nat → data) → datastream
butlastn	datastream	f	nat × datalist → datalist
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	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
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
lastn	datastream	f	nat × datalist → datalist
m	nat-basic1	v	nat
m0	nat-inf-basic	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	datastream	f	data × nat → datalist
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
restn	datastream	f	nat × datalist → datalist
rev	datastream	f	datalist → datalist
rmdup	datastream	f	datalist → datalist
sublist	datastream	f	nat × nat × datalist → datalist
tl	datastream	f	datastream → datastream