[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
# .	stringset	f	stringset → nat
# .	posix-history	f	posix-history → nat
# .	path	f	path → nat
. '	posix-history	f	posix-event → posix-history
. '	path	f	string → path
. + .	posix-history	f	posix-event × posix-event → posix-history
. + .	nat-basic2	f	nat × nat → nat
. + .	posix-history	f	posix-history × posix-event → posix-history
. + .	buffer	f	buffer × buffer → buffer
. + .	posix-history	f	posix-history × posix-history → posix-history
. + .	string-data	f	char × string → string
. + .	posix-history	f	posix-event × posix-history → posix-history
. + .	path	f	string × string → path
. + .	path	f	string × path → path
. + .	path	f	path × string → path
. + .	path	f	path × path → path
. ++ .	stringset	f	stringset × string → stringset
. ++ .	path	f	path × string → path
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	stringset	f	stringset × string → stringset
. -1	nat-basic1	f	nat → nat
. -1l .	path	f	path × nat → path
. -1l .	path	f	path × string → path
. -l .	path	f	path × string → path
. .buf	posix-event	f	posix-event → buffer
. .char1	string-data	f	string → char
. .directory	inode	p	inode
. .directory:= .	inode	f	inode × bool → inode
. .err	posix-event	f	posix-event → error
. .fd	posix-event	f	posix-event → nat
. .first	path	f	path → string
. .first	posix-history	f	posix-history → posix-event
. .ino	inode	f	inode → nat
. .ino:= .	inode	f	inode × nat → inode
. .last	path	f	path → string
. .meta	inode	f	inode → metadata
. .meta	posix-event	f	posix-event → metadata
. .meta:= .	inode	f	inode × metadata → inode
. .mode	posix-event	f	posix-event → mode
. .n	posix-event	f	posix-event → nat
. .names	posix-event	f	posix-event → stringset
. .nlink	inode	f	inode → nat
. .nlink:= .	inode	f	inode × nat → inode
. .path	posix-event	f	posix-event → path
. .path'	posix-event	f	posix-event → path
. .rest	posix-history	f	posix-history → posix-history
. .rest	path	f	path → path
. .rstring	string-data	f	string → string
. .size	inode	f	inode → nat
. .size:= .	inode	f	inode × nat → inode
. .whence	posix-event	f	posix-event → seekflag
. < .	posix-history	p	posix-history × posix-history
. < .	path	p	path × path
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	buffer	f	buffer × nat → data
. [ . ]	path	f	path × nat × string → path
. [ . ]	buffer	f	buffer × nat × data → buffer
. [ . ]	path	f	path × nat → string
. \ .	stringset	f	stringset × stringset → stringset
. ∈ .	posix-history	p	posix-event × posix-history
. ∈ .	path	p	string × path
. ∈ .	stringset	p	string × stringset
. ∈ .	buffer	p	data × buffer
. ∩ .	stringset	f	stringset × stringset → stringset
. ∪ .	stringset	f	stringset × stringset → stringset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	stringset	p	stringset × stringset
. ⊑ .	path	p	path × path
. ⊒ .	path	p	path × path
[]	posix-history	c	posix-history
{ . }	stringset	f	string → stringset
ε	path	c	path
∅	stringset	c	stringset
⌊ . ⌋	error-class	p	error
EACCESS	error	c	error
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
ENOENT	error	c	error
ENOMEM	error	c	error
ENOSPC	error	c	error
ENOTDIR	error	c	error
ENOTEMPTY	error	c	error
ERR	error-class	v	error,flexible
ESUCCESS	error	c	error
MODE_R	mode	c	mode
MODE_RW	mode	c	mode
MODE_W	mode	c	mode
SEEK_CUR	seekflag	c	seekflag
SEEK_END	seekflag	c	seekflag
SEEK_SET	seekflag	c	seekflag
boolvar	inode	v	bool
boolvar0	inode	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
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
close	posix-event	f	nat × error → posix-event
cmp	buffer	p	buffer × data × nat × nat
cmp	buffer	p	buffer × nat × buffer × nat × nat
copy	buffer	f	buffer × nat × buffer × nat × nat → buffer
crash	posix-event	c	posix-event
create	posix-event	f	path × metadata × error → posix-event
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
disj	path	p	path × path
dups	path	p	path
empty	buffer	c	data
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
fail#	error-class	pr	: error
fail_or_success#	error-class	pr	: error
fill	buffer	f	buffer × data × nat × nat → buffer
fill	buffer	f	buffer × data → buffer
fillfirst	path	f	nat × string × path → path
firstn	path	f	nat × path → path
frome	path	f	path × string → path
id○	buffer	p	buffer × buffer × nat
idrange	buffer	p	buffer × nat × nat
inode	inode	s
inode	inode	v	inode
lastn	path	f	nat × path → path
link	posix-event	f	path × path × error → posix-event
m	nat-basic1	v	nat
m0	inode	v	nat
m1	inode	v	nat
m2	inode	v	nat
m3	inode	v	nat
m4	inode	v	nat
max	min-max	f	nat × nat → nat
md	metadata	v	metadata
md0	inode	v	metadata
metadata	metadata	s
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkdir	posix-event	f	path × metadata × error → posix-event
mkempbuf	buffer	f	nat → buffer
mkinode	inode	f	nat × metadata × bool × nat × nat → inode
mkpath	path	f	string × nat → path
mkzbuf	buffer	f	nat → buffer
mode	mode	s
mode	mode	v	mode
mode0	posix-event	v	mode
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
open	posix-event	f	path × nat × mode × error → posix-event
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
posix-event	posix-event	s
posix-event	posix-event	v	posix-event
posix-event0	posix-history	v	posix-event
posix-event1	posix-history	v	posix-event
posix-event2	posix-history	v	posix-event
posix-history	posix-history	s
pxh	posix-history	v	posix-history
pxh0	posix-history	v	posix-history
pxh1	posix-history	v	posix-history
pxh10	posix-history	v	posix-history
pxh2	posix-history	v	posix-history
pxh3	posix-history	v	posix-history
pxh4	posix-history	v	posix-history
pxh5	posix-history	v	posix-history
pxh6	posix-history	v	posix-history
pxh7	posix-history	v	posix-history
pxh8	posix-history	v	posix-history
pxh9	posix-history	v	posix-history
q	path	v	path
q0	path	v	path
q1	path	v	path
q2	path	v	path
range=	buffer	p	buffer × nat × buffer × nat × nat
read	posix-event	f	nat × buffer × nat × error → posix-event
readdir	posix-event	f	path × stringset × error → posix-event
readmeta	posix-event	f	path × metadata × error → posix-event
renam	posix-event	f	path × path × error → posix-event
resize	buffer	f	buffer × nat → buffer
restn	path	f	nat × path → path
rev	buffer	f	buffer → buffer
rev	buffer	f	buffer × nat → buffer
rev	path	f	path → path
rmdir	posix-event	f	path × error → posix-event
rmdup	path	f	path → path
seek	posix-event	f	nat × nat × seekflag × error → posix-event
seekflag	seekflag	s
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
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
strings	stringset	v	stringset
strings0	stringset	v	stringset
strings1	stringset	v	stringset
strings2	stringset	v	stringset
stringset	stringset	s
subarray	buffer	f	buffer × nat × nat → buffer
sublist	path	f	nat × nat × path → path
truncate	posix-event	f	path × nat × error → posix-event
unlink	posix-event	f	path × error → posix-event
whence	seekflag	v	seekflag
whence0	posix-event	v	seekflag
write	posix-event	f	nat × buffer × nat × error → posix-event
writemeta	posix-event	f	path × metadata × error → posix-event
zero	buffer	c	data