[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
# .	string	f	string → nat
# .	pcache	f	key-set → nat
# .	buffer	f	buffer → nat
# .	pcache	f	pcache → 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
. + .	string	f	char × string → string
. + .	buffer	f	buffer × buffer → buffer
. + .	string	f	string × string → string
. + .	string	f	string × char → string
. ++ .	pcache	f	key-set × key → key-set
. ++ .	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
. -- .	pcache	f	pcache × key → pcache
. -- .	pcache	f	key-set × key → key-set
. -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 ≠ ""
. .data?	key	p	key
. .dentry?	key	p	key
. .dirty	pcache-entry	p	pcache-entry
. .dirty:= .	pcache-entry	f	pcache-entry × bool → pcache-entry
. .ino	key	f	key → nat
. .ino:= .	key	f	key × nat → key
. .inode?	key	p	key
. .last	string	pf	string → char with λ str. str ≠ ""
. .name	key	pf	key → string with λ key. key.dentry?
. .name:= .	key	pf	key × string → key with λ key, str. key.dentry?
. .page	pcache-entry	f	pcache-entry → buffer
. .page:= .	pcache-entry	f	pcache-entry × buffer → pcache-entry
. .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 ≠ ""
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	pcache	pf	pcache × key → pcache-entry with λ pcache, key. key ∈ pcache
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	pcache	f	pcache × key × pcache-entry → pcache
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. \ .	pcache	f	key-set × key-set → key-set
. \ .	pcache	f	pcache × key-set → pcache
. \| .	pcache	f	pcache × key-set → pcache
. ∈ .	pcache	p	pcache-entry × pcache
. ∈ .	pcache	p	key × key-set
. ∈ .	pcache	p	key × pcache
. ∈ .	string	p	char × string
. ∈ .	buffer	p	data × buffer
. ∩ .	pcache	f	key-set × key-set → key-set
. ∪ .	pcache	f	key-set × key-set → key-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	pcache	p	key-set × key-set
. ⊆ .	pcache	p	pcache × pcache
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
. ⊕ .	pcache	f	pcache × pcache → pcache
{ . }	pcache	f	key → key-set
∅	pcache	c	pcache
∅	pcache	c	key-set
⊏	string	p	string × string
VFS_PAGE_SIZE	page	c	nat
boolvar	pcache-entry	v	bool
boolvar0	pcache-entry	v	bool
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
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
dentrykey	key	f	nat × string → key
disj	string	p	string × string
dom .	pcache	f	pcache → key-set
dups	string	p	string
empty	buffer	c	data
evict	pcache-del-ops	f	nat × pcache → pcache
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
ino	pcache-del-ops	v	nat
ino0	pcache-del-ops	v	nat
inodekey	key	f	nat → key
key	key	s
key	key	v	key
key-set	pcache	s
key1	pcache	v	key
key2	pcache	v	key
ks	pcache	v	key-set
ks0	pcache	v	key-set
ks1	pcache	v	key-set
ks2	pcache	v	key-set
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
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
mkpentry	pcache-entry	f	bool × buffer → pcache-entry
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
name	pcache-del-ops	v	string
nat	nat-basic	s
pageno	pcache-del-ops	v	nat
pcache	pcache	v	pcache
pcache	pcache	s
pcache-entry	pcache-entry	s
pcache0	pcache	v	pcache
pcache1	pcache	v	pcache
pcache2	pcache	v	pcache
pe	pcache-entry	v	pcache-entry
pe0	pcache	v	pcache-entry
pe1	pcache	v	pcache-entry
pe2	pcache	v	pcache-entry
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	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
rev	string	f	string → string
rmdup	string	f	string → string
size	pcache-del-ops	v	nat
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
truncate	pcache-del-ops	f	nat × nat × pcache → pcache
zero	buffer	c	data
zeropage	page	c	buffer