[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
# .	string	f	string → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	string	f	char → string
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	string	f	string × char → string
. + .	string	f	char × string → string
. + .	string	f	string × string → string
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -l .	string	f	string × char → string
. -p .	string	f	string × nat → string
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .last	string	pf	string → char with λ str. str ≠ ""
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .toString	debug	f	nat → string
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. ∈ .	string	p	char × string
. ∈ .	buffer	p	data × buffer
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
⊏	string	p	string × string
⌊ . ⌋	error-class	p	error
EACCESS	error	c	error
EB_PAGE_SIZE	eraseblock	c	nat
EBADFD	error	c	error
ECOMMIT	error	c	error
EEXISTS	error	c	error
EFAIL	error	c	error
EINVAL	error	c	error
EIO	error	c	error
EISDIR	error	c	error
ENCODED_ELEM_SIZE	encoding-elem-size	c	nat
ENOENT	error	c	error
ENOMEM	error	c	error
ENOSPC	error	c	error
ENOTDIR	error	c	error
ENOTEMPTY	error	c	error
EROFS	error	c	error
ERR	error-class	v	error,flexible
ERR0	error-class	v	error,flexible
ESUCCESS	error	c	error
EUCLEAN	error	c	error
LEB_SIZE	eraseblock	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
a	elem	v	elem
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
b	elem	v	elem
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
c	elem	v	elem
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	buffer	pf	buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
debug#	debug	pr	string :
decode#	encoding	pr	nat × buffer : elem × nat : error (nondeterministic)
decode_nonempty#	encoding-fixed-size-nonempty	pr	nat × buffer : elem : error (nondeterministic)
disj	string	p	string × string
dups	string	p	string
elem	elem	s
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
encode#	encoding	pr	elem × nat : buffer × nat : error (nondeterministic)
encode_nonempty#	encoding-fixed-size-nonempty	pr	elem × nat : buffer : error (nondeterministic)
encoding-size	encoding	f	elem → nat
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
fail#	error-class	pr	: : error (nondeterministic)
fail_or_success#	error-class	pr	: : error (nondeterministic)
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
fillfirst	string	f	nat × char × string → string
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
is-aligned	align	p	nat × nat
is-encoded	encoding	p	elem × buffer
is-encoded-nonempty	encoding-fixed-size-nonempty	p	elem × buffer
is-garbage	encoding	p	buffer
is-garbage-nonempty	encoding-fixed-size-nonempty	p	buffer
isempty	eraseblock	p	buffer
isempty	eraseblock	p	buffer × nat × nat
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	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	string	f	char × nat → string
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
pos	string	f	char × string → nat
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	string	f	string → string
rmdup	string	f	string → string
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
zero	buffer	c	data