[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
# .	path	f	path → nat
. '	path	f	string → path
. + .	string-data	f	char × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	path	f	string × string → path
. + .	path	f	string × path → path
. + .	path	f	path × string → path
. + .	path	f	path × path → path
. ++ .	path	f	path × string → path
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	path	f	path × nat → path
. -1l .	path	f	path × string → path
. -l .	path	f	path × string → path
. .char1	string-data	f	string → char
. .first	path	f	path → string
. .last	path	f	path → string
. .rest	path	f	path → path
. .rstring	string-data	f	string → string
. < .	path	p	path × path
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	path	f	path × nat → string
. [ . ]	path	f	path × nat × string → path
. ∈ .	path	p	string × path
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	path	p	path × path
. ⊒ .	path	p	path × path
ε	path	c	path
butlastn	path	f	nat × path → path
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
disj	path	p	path × path
dups	path	p	path
fillfirst	path	f	nat × string × path → path
firstn	path	f	nat × path → path
frome	path	f	path × string → path
lastn	path	f	nat × path → path
m	nat-basic1	v	nat
md	metadata	v	metadata
meta	permission-param	f	path × state → metadata
metadata	metadata	s
mkpath	path	f	string × nat → path
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
p	path	v	path
p'	path	v	path
p0	path	v	path
p1	path	v	path
p2	path	v	path
p3	path	v	path
p4	path	v	path
p5	path	v	path
parent	path	f	path → path
path	path	s
pos	path	f	string × path → nat
pr	permission	p	user × metadata
pr	path-permission	p	user × path × state
pw	path-permission	p	user × path × state
pw	permission	p	user × metadata
px	permission	p	user × metadata
px	path-permission	p	user × path × state
py	path-permission	p	user × path × state
q	path	v	path
q0	path	v	path
q1	path	v	path
q2	path	v	path
restn	path	f	nat × path → path
rev	path	f	path → path
rmdup	path	f	path → path
st	permission-param	v	state
state	permission-param	s
str	string-data	v	string
str0	string-data	v	string
str1	string-data	v	string
str2	string-data	v	string
str3	string-data	v	string
string	string-data	s
sublist	path	f	nat × nat × path → path
user	user	v	user
user	user	s