| Symbol | Specification | Kind | Type |
|---|---|---|---|
| -∞ | int-inf-basic | c | intinf |
| . +1 | int-basic1 | f | int → int |
| . -1 | int-basic1 | f | int → int |
| . .i | int-inf-basic | pf | intinf → int with λ i∞. i∞ ≠ ∞ ∧ i∞ ≠ -∞ |
| . < . | int-basic1 | p | int × int |
| ∞ | int-inf-basic | c | intinf |
| ⌜ . ⌝ | int-inf-basic | f | int → intinf |
| i | int-inf-basic | v | int |
| i∞ | int-inf-basic | v | intinf |
| int | int-basic1 | s | |
| intinf | int-inf-basic | s |