[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
# .	node-list	f	node-list → nat
# .	string	f	string → nat
. '	node-list	f	node → node-list
. '	string	f	char → string
. + .	nat-basic	f	nat × nat → nat
. + .	node-list	f	node-list × node → node-list
. + .	buffer	f	buffer × buffer → buffer
. + .	node-list	f	node-list × node-list → node-list
. + .	string	f	char × string → string
. + .	node-list	f	node × node-list → node-list
. + .	string	f	string × string → string
. + .	string	f	string × char → string
. ++ .	node-list	f	node-list × node → node-list
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	node-list	f	node × node → node-list
. - .	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
. -1l .	node-list	f	node-list × node → node-list
. -l .	string	f	string × char → string
. -l .	node-list	f	node-list × node → node-list
. -p .	node-list	f	node-list × nat → node-list
. -p .	string	f	string × nat → string
. .butlast	node-list	pf	node-list → node-list with λ ndx. ndx ≠ []
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .data	node	pf	node → buffer with λ nd. nd.data?
. .data:= .	node	pf	node × buffer → node with λ nd, buf. nd.data?
. .data?	key	p	key
. .data?	node	p	node
. .dentry?	key	p	key
. .dentry?	node	p	node
. .directory	node	pp	node with λ nd. nd.inode?
. .directory:= .	node	pf	node × bool → node with λ nd, boolvar. nd.inode?
. .head	node-list	pf	node-list → node with λ ndx. ndx ≠ []
. .ino	key	f	key → nat
. .ino	node	pf	node → nat with λ nd. nd.dentry?
. .ino:= .	key	f	key × nat → key
. .ino:= .	node	pf	node × nat → node with λ nd, m. nd.dentry?
. .inode?	node	p	node
. .inode?	key	p	key
. .key	node	f	node → key
. .key:= .	node	f	node × key → node
. .last	node-list	pf	node-list → node with λ ndx. ndx ≠ []
. .last	string	pf	string → char with λ str. str ≠ ""
. .meta	node	pf	node → metadata with λ nd. nd.inode?
. .meta:= .	node	pf	node × metadata → node with λ nd, md. nd.inode?
. .name	key	pf	key → string with λ key. key.dentry?
. .name:= .	key	pf	key × string → key with λ key, str. key.dentry?
. .nlink	node	pf	node → nat with λ nd. nd.inode?
. .nlink:= .	node	pf	node × nat → node with λ nd, m. nd.inode?
. .nsubdirs	node	pf	node → nat with λ nd. nd.inode?
. .nsubdirs:= .	node	pf	node × nat → node with λ nd, m. nd.inode?
. .part	key	pf	key → nat with λ key. key.data?
. .part:= .	key	pf	key × nat → key with λ key, m. key.data?
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	node	pf	node → nat with λ nd. nd.trunc? ∨ nd.inode?
. .size:= .	node	pf	node × nat → node with λ nd, m. nd.trunc? ∨ nd.inode?
. .tail	node-list	pf	node-list → node-list with λ ndx. ndx ≠ []
. .trunc?	node	p	node
. < .	nat-basic	p	nat × nat
. < .	node-list	p	node-list × node-list
. > .	nat	p	nat × nat
. [ . ]	node-list	pf	node-list × nat × node → node-list with λ ndx, n, nd. n < # ndx
. [ . ]	node-list	pf	node-list × nat → node with λ ndx, n. n < # ndx
. [ . ]	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
. ∈ .	buffer	p	data × buffer
. ∈ .	node-list	p	node × node-list
. ∈ .	string	p	char × string
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	node-list	p	node-list × node-list
. ⊑ .	string	p	string × string
. ⊒ .	node-list	p	node-list × node-list
. ⊒ .	string	p	string × string
[]	node-list	c	node-list
⊏	string	p	string × string
VFS_PAGE_SIZE	page	c	nat
boolvar	node	v	bool
boolvar0	node	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	node-list	pf	nat × node-list → node-list with λ n, ndx. n ≤ # ndx
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
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
datakey	key	f	nat × nat → key
datanode	node	f	key × buffer → node
dentrykey	key	f	nat × string → key
dentrynode	node	f	key × nat → node
disj	node-list	p	node-list × node-list
disj	string	p	string × string
dropn	node-list	f	nat × node-list → node-list
dups	node-list	p	node-list
dups	string	p	string
empty	buffer	c	data
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fillfirst	string	f	nat × char × string → string
fillfirst	node-list	f	nat × node × node-list → node-list
firstn	node-list	pf	nat × node-list → node-list with λ n, ndx. n ≤ # ndx
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
frome	node-list	f	node-list × node → node-list
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
inodekey	key	f	nat → key
inodenode	node	f	key × metadata × bool × nat × nat × nat → node
key	key	s
key	key	v	key
key0	node	v	key
lastn	node-list	pf	nat × node-list → node-list with λ n, ndx. n ≤ # ndx
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	key	v	nat
m1	key	v	nat
m2	key	v	nat
m3	node	v	nat
m4	node	v	nat
max	min-max	f	nat × nat → nat
md	metadata	v	metadata
md0	node	v	metadata
metadata	metadata	s
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	node-list	f	node × nat → node-list
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
nd	node	v	node
nd0	node	v	node
nd1	node	v	node
nd2	node	v	node
nd3	node	v	node
ndx	node-list	v	node-list
ndx0	node-list	v	node-list
ndx1	node-list	v	node-list
ndy	node-list	v	node-list
ndz	node-list	v	node-list
node	node	s
node-list	node-list	s
pos	string	f	char × string → nat
pos	node-list	f	node × node-list → nat
prefixn	node-list	f	nat × node-list → node-list
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	node-list	pf	nat × node-list → node-list with λ n, ndx. n ≤ # ndx
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	node-list	f	node-list → node-list
rev	string	f	string → string
rmdup	string	f	string → string
rmdup	node-list	f	node-list → node-list
slice	node-list	f	nat × nat × node-list → node-list
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	node-list	pf	nat × nat × node-list → node-list with λ n, m, ndx. n + m ≤ # ndx
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
truncnode	node	f	key × nat → node
zero	buffer	c	data
zeropage	page	c	buffer