[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
# .	key-list-set	f	key-set → nat
# .	string	f	string → nat
# .	key-list-set	f	key-list → nat
. '	key-list-set	f	key → key-list
. '	string	f	char → string
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	key-list-set	f	key-list × key → key-list
. + .	string	f	string × string → string
. + .	key-list-set	f	key-list × key-list → key-list
. + .	string	f	string × char → string
. + .	key-list-set	f	key × key-list → key-list
. ++ .	key-list-set	f	key-set × key → key-set
. ++ .	string	f	string × char → string
. ++ .	key-list-set	f	key-list × key → key-list
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	key-list-set	f	key × key → key-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	key-list-set	f	key-set × key → key-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	key-list-set	f	key-list × key → key-list
. -l .	string	f	string × char → string
. -l .	key-list-set	f	key-list × key → key-list
. -p .	key-list-set	f	key-list × nat → key-list
. -p .	string	f	string × nat → string
. .butlast	key-list-set	pf	key-list → key-list with λ kx. kx ≠ []
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .data?	key	p	key
. .dentry?	key	p	key
. .head	key-list-set	pf	key-list → key with λ kx. kx ≠ []
. .ino	key	f	key → nat
. .ino:= .	key	f	key × nat → key
. .inode?	key	p	key
. .last	key-list-set	pf	key-list → key with λ kx. kx ≠ []
. .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?
. .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 ≠ ""
. .tail	key-list-set	pf	key-list → key-list with λ kx. kx ≠ []
. .toSet	key-list-set	f	key-list → key-set
. < .	key-list-set	p	key-list × key-list
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	key-list-set	pf	key-list × nat × key → key-list with λ kx, n, key. n < # kx
. [ . ]	key-list-set	pf	key-list × nat → key with λ kx, n. n < # kx
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. \ .	key-list-set	f	key-set × key-set → key-set
. ∈ .	key-list-set	p	key × key-set
. ∈ .	string	p	char × string
. ∈ .	key-list-set	p	key × key-list
. ∩ .	key-list-set	f	key-set × key-set → key-set
. ∪ .	key-list-set	f	key-set × key-set → key-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	key-list-set	p	key-set × key-set
. ⊑ .	string	p	string × string
. ⊑ .	key-list-set	p	key-list × key-list
. ⊒ .	key-list-set	p	key-list × key-list
. ⊒ .	string	p	string × string
[]	key-list-set	c	key-list
{ . }	key-list-set	f	key → key-set
∅	key-list-set	c	key-set
⊏	string	p	string × string
butlastn	key-list-set	pf	nat × key-list → key-list with λ n, kx. n ≤ # kx
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
datakey	key	f	nat × nat → key
dentrykey	key	f	nat × string → key
disj	key-list-set	p	key-list × key-list
disj	string	p	string × string
dropn	key-list-set	f	nat × key-list → key-list
dups	key-list-set	p	key-list
dups	string	p	string
fillfirst	string	f	nat × char × string → string
fillfirst	key-list-set	f	nat × key × key-list → key-list
firstn	key-list-set	pf	nat × key-list → key-list with λ n, kx. n ≤ # kx
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
frome	key-list-set	f	key-list × key → key-list
inodekey	key	f	nat → key
key	key	s
key	key	v	key
key-list	key-list-set	s
key-set	key-list-set	s
key0	key-list-set	v	key
key1	key-list-set	v	key
key2	key-list-set	v	key
ks	key-list-set	v	key-set
ks0	key-list-set	v	key-set
ks1	key-list-set	v	key-set
ks2	key-list-set	v	key-set
kx	key-list-set	v	key-list
kx0	key-list-set	v	key-list
kx1	key-list-set	v	key-list
ky	key-list-set	v	key-list
kz	key-list-set	v	key-list
lastn	key-list-set	pf	nat × key-list → key-list with λ n, kx. n ≤ # kx
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
mklist	string	f	char × nat → string
mklist	key-list-set	f	key × nat → key-list
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
pos	key-list-set	f	key × key-list → nat
prefixn	key-list-set	f	nat × key-list → key-list
restn	key-list-set	pf	nat × key-list → key-list with λ n, kx. n ≤ # kx
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	string	f	string → string
rev	key-list-set	f	key-list → key-list
rmdup	string	f	string → string
rmdup	key-list-set	f	key-list → key-list
slice	key-list-set	f	nat × nat × key-list → key-list
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
sublist	key-list-set	pf	nat × nat × key-list → key-list with λ n, m, kx. n + m ≤ # kx
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str