| 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 | p | Intinf × Intinf |
| ∞ | int-inf-basic | c | Intinf |
| ⌜ . ⌝ | int-inf-basic | f | Int → Intinf |
| Int | int-basic1 | s | |
| Intinf | int-inf-basic | s | |
| i | int-inf | v | Int |
| i∞ | int-inf | v | Intinf |