[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
. % .	nat-div	f	nat × nat → nat
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic2	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. / .	nat-div	f	nat × nat → nat
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	buffer	f	buffer × nat → data
. [ . ]	buffer	f	buffer × nat × data → buffer
. ∈ .	buffer	p	data × buffer
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
EB_PAGE_SIZE	eraseblock	c	nat
LEB_SIZE	eraseblock	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	buffer	p	buffer × data × nat × nat
cmp	buffer	p	buffer × nat × buffer × 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
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
fill	buffer	f	buffer × data × nat × nat → buffer
fill	buffer	f	buffer × data → buffer
id○	buffer	p	buffer × buffer × nat
idrange	buffer	p	buffer × nat × nat
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer
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
mkzbuf	buffer	f	nat → buffer
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	buffer	f	buffer → buffer
rev	buffer	f	buffer × nat → buffer
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	f	buffer × nat × nat → buffer
zero	buffer	c	data