| Symbol | Specification | Kind | Type |
|---|---|---|---|
| . + . | nat-basic2 | f | nat × nat → nat |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . .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 |
| . .size | inode | f | inode → nat |
| . .size:= . | inode | f | inode × nat → inode |
| . < . | nat-basic1 | 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-basic1 | v | nat |
| m0 | inode | v | nat |
| m1 | inode | v | nat |
| m2 | inode | v | nat |
| m3 | inode | v | nat |
| m4 | inode | v | nat |
| md | metadata | v | metadata |
| md0 | inode | v | metadata |
| metadata | metadata | s | |
| mkinode | inode | f | nat × metadata × bool × nat × nat → inode |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s |