[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
# .	natstream	f	natstream → natinf
# .	natstream	f	natlist → nat
. '	natstream	f	nat → natlist
. + .	nat-basic2	f	nat × nat → nat
. + .	natstream	f	natstream × natstream → natstream
. + .	natstream	f	nat × natlist → natlist
. + .	natstream	f	nat × natstream → natstream
. + .	natstream	f	natlist × natlist → natlist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	natstream	f	natlist × nat → natlist
. ++ .	natstream	f	natlist × nat → natlist
. +1	nat-basic1	f	nat → nat
. +l .	natstream	f	nat × nat → natlist
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	natstream	f	natlist × nat → natlist
. -l .	natstream	f	natlist × nat → natlist
. -pos .	natstream	f	natlist × nat → natlist
. .butlast	natstream	f	natlist → natlist
. .f	natstream	f	natstream → nat → nat
. .first	natstream	f	natlist → nat
. .l	natstream	f	natstream → natlist
. .last	natstream	f	natlist → nat
. .n	nat-inf-basic	f	natinf → nat
. .rest	natstream	f	natlist → natlist
. < .	nat-inf	p	natinf × natinf
. < .	natstream	p	natlist × natlist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	natstream	f	natlist × nat → nat
. [ . ]	natstream	f	natlist × nat × nat → natlist
. [ . ]	natstream	f	natstream × nat × nat → natstream
. [ . ]	natstream	f	natstream × nat → nat
. ∈ .	natstream	p	nat × natlist
. ≤ .	natstream	p	natstream × natstream
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	natstream	p	natstream × natstream
. ⊑ .	natstream	p	natlist × natlist
. ⊒ .	natstream	p	natlist × natlist
. from .	natstream	f	natstream × nat → natstream
. from .	natstream	f	(nat → nat) × nat → nat → nat
. from .	natstream	f	natlist × nat → natlist
. to .	natstream	f	natstream × nat → natstream
. to .	natstream	f	(nat → nat) × nat → natlist
. to .	natstream	f	natlist × nat → natlist
. to∞ .	natstream	f	natstream × natinf → natstream
[]	natstream	c	natlist
[]	natstream	c	natstream
∞	nat-inf-basic	c	natinf
⌜ . ⌝	nat-inf-basic	f	nat → natinf
⌜ . ⌝	natstream	f	natlist → natstream
⌜ . ⌝	natstream	f	(nat → nat) → natstream
butlastn	natstream	f	nat × natlist → natlist
cnt	natstream	f	nat × natstream → natinf
disj	natstream	p	natlist × natlist
dups	natstream	p	natlist
fillfirst	natstream	f	nat × nat × natlist → natlist
filter	natstream	f	(nat → bool) × natstream → natstream
finp	natstream	p	natstream
firstn	natstream	f	nat × natlist → natlist
frome	natstream	f	natlist × nat → natlist
hd	natstream	f	natstream → nat
lastn	natstream	f	nat × natlist → natlist
lastoc	natstream	f	nat × natstream → natinf
lim	natstream	f	(nat → natstream) → natstream
m	nat-basic1	v	nat
m0	nat-inf-basic	v	nat
m1	natstream	v	nat
m2	natstream	v	nat
m3	natstream	v	nat
m4	natstream	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	natstream	f	nat × nat → natlist
mon	natstream	p	(nat → natstream)
n	nat-basic1	v	nat
nσ	natstream	v	natstream
nσ0	natstream	v	natstream
nσ1	natstream	v	natstream
nσ2	natstream	v	natstream
nσf	natstream	v	nat → natstream
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
natlist	natstream	s
natstream	natstream	s
nl	natstream	v	natlist
nl0	natstream	v	natlist
nl1	natstream	v	natlist
nl10	natstream	v	natlist
nl2	natstream	v	natlist
nl3	natstream	v	natlist
nl4	natstream	v	natlist
nl5	natstream	v	natlist
nl6	natstream	v	natlist
nl7	natstream	v	natlist
nl8	natstream	v	natlist
nl9	natstream	v	natlist
nnf	mon-lim-filter-count	v	nat → nat
nnf0	natstream	v	nat → nat
nnf1	natstream	v	nat → nat
np	mon-lim-filter-count	v	nat → bool
np0	natstream	v	nat → bool
pos	natstream	f	nat × natlist → nat
rem	natstream	f	natstream × (nat → bool) → natstream
restn	natstream	f	nat × natlist → natlist
rev	natstream	f	natlist → natlist
rmdup	natstream	f	natlist → natlist
sublist	natstream	f	nat × nat × natlist → natlist
tl	natstream	f	natstream → natstream