| Symbol | Specification | Kind | Type |
|---|---|---|---|
| . left | node | f | Node[A] → Ref[Node[A]] |
| . left:= . | node | f | Node[A] × Ref[Node[A]] → Node[A] |
| . right | node | f | Node[A] → Ref[Node[A]] |
| . right:= . | node | f | Node[A] × Ref[Node[A]] → Node[A] |
| . val | node | f | Node[A] → A |
| . val:= . | node | f | Node[A] × A → Node[A] |
| Node | node | s | |
| Ref | polyref | s | |
| left | node | v | Ref[Node[A]] |
| mknode | node | f | Ref[Node[A]] × A × Ref[Node[A]] → Node[A] |
| nd | node | v | Node[A] |
| null | polyref | c | Ref[A] |
| right | node | v | Ref[Node[A]] |
| val | node | v | A |