Signature symbols in this unit

Symbol	Specification	Kind	Type
. + .	nat-basic	f	nat × nat → nat
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .directory	inode	p	inode
. .directory:= .	inode	f	inode × bool → inode
. .ino	inode	f	inode → nat
. .ino:= .	inode	f	inode × nat → inode
. .meta	inode	f	inode → metadata
. .meta:= .	inode	f	inode × metadata → inode
. .nlink	inode	f	inode → nat
. .nlink:= .	inode	f	inode × nat → inode
. .nsubdirs	inode	f	inode → nat
. .nsubdirs:= .	inode	f	inode × nat → inode
. .size	inode	f	inode → nat
. .size:= .	inode	f	inode × nat → inode
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
boolvar	inode	v	bool
boolvar0	inode	v	bool
inode	inode	s
inode	inode	v	inode
m	nat-basic	v	nat
m0	inode	v	nat
m1	inode	v	nat
m2	inode	v	nat
m3	inode	v	nat
m4	inode	v	nat
m5	inode	v	nat
m6	inode	v	nat
md	metadata	v	metadata
md0	inode	v	metadata
metadata	metadata	s
mkinode	inode	f	nat × metadata × bool × nat × nat × nat → inode
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s