[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
# .	buffer	f	buffer → nat
# .	list-data	f	list → nat
. '	list	f	elem → list
. + .	nat-basic2	f	nat × nat → nat
. + .	list	f	elem × elem → list
. + .	buffer	f	buffer × buffer → buffer
. + .	list	f	list × elem → list
. + .	list-data	f	elem × list → list
. + .	list	f	list × list → list
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. .butlast	list-last	f	list → list
. .first	list-data	f	list → elem
. .last	list-last	f	list → elem
. .rest	list-data	f	list → list
. < .	list-data	p	list × list
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	buffer	f	buffer × nat → data
. [ . ]	buffer	f	buffer × nat × data → buffer
. ∈ .	list	p	elem × list
. ∈ .	buffer	p	data × buffer
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	list-last	p	list × list
. ⊒ .	list-last	p	list × list
[]	list-data	c	list
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	list-last	f	nat × list → list
c	elem	v	elem
cmp	buffer	p	buffer × nat × buffer × nat × nat
cmp	buffer	p	buffer × data × nat × nat
copy	buffer	f	buffer × nat × buffer × nat × nat → buffer
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
disj	list-dup	p	list × list
dups	list-dup	p	list
elem	elem	s
empty	buffer	c	data
fill	buffer	f	buffer × data × nat × nat → buffer
fill	buffer	f	buffer × data → buffer
fillfirst	list-last	f	nat × elem × list → list
id○	buffer	p	buffer × buffer × nat
idrange	buffer	p	buffer × nat × nat
list	list-data	s
m	nat-basic1	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	list-last	f	elem × nat → list
mkzbuf	buffer	f	nat → buffer
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pack	elem-repr	f	elem → buffer
pack	elem-list-repr	f	list → buffer
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	buffer	f	buffer → buffer
rev	list-last	f	list → list
rev	buffer	f	buffer × nat → buffer
rmdup	list-dup	f	list → list
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	f	buffer × nat × nat → buffer
unpack	elem-repr	f	buffer → elem
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list
zero	buffer	c	data