| Symbol | Specification | Kind | Type |
|---|
| # . | set-basic | f | set('a) → nat |
| # . | array | f | array('a) → nat |
| #c . | matrix | f | matrix('a) → nat |
| #r . | matrix | f | matrix('a) → nat |
| . * . | ring | f | ring × ring → ring |
| . * . | matrixops | pf | matrix(ring) × matrix(ring) → matrix(ring) with λ mx1, mx2. #c mx1 = #r mx2 |
| . * . | matrixops | pf | matrix(ring) × array(ring) → array(ring) with λ mx, vec. #r mx = # vec |
| . * . | matrixops | pf | array(ring) × matrix(ring) → array(ring) with λ vec, mx. #c mx = # vec |
| . * . | matrixops | pf | array(ring) × array(ring) → ring with λ vec1, vec2. # vec1 = # vec2 |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | ring | f | ring × ring → ring |
| . + . | matrixops | pf | matrix(ring) × matrix(ring) → matrix(ring) with λ mx1, mx2. #r mx1 = #r mx2 ∧ #c mx2 = #c mx2 |
| . + . | matrixops | pf | array(ring) × array(ring) → array(ring) with λ vec1, vec2. # vec1 = # vec2 |
| . ++ . | set-basic | f | set('a) × 'a → set('a) |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | set-union | f | set('a) × 'a → set('a) |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . := . ] | matrix | pf | matrix('a) × nat × nat × 'a → matrix('a) with λ mx, r, c, a. r < #r mx ∧ c < #c mx |
| . [ . := . ] | array | pf | array('a) × nat × 'a → array('a) with λ ar, n, a. n < # ar |
| . [ . ] | matrix | pf | matrix('a) × nat × nat → 'a with λ mx, r, c. r < #r mx ∧ c < #c mx |
| . [ . ] | array | pf | array('a) × nat → 'a with λ ar, n. n < # ar |
| . [ . ]c | matrix+array | pf | matrix('a) × nat → array('a) with λ mx, c. c < #c mx |
| . [ . ]r | matrix+array | pf | matrix('a) × nat → array('a) with λ mx, r. r < #r mx |
| . \ . | set-union | f | set('a) × set('a) → set('a) |
| . ∈ . | set-basic | p | 'a × set('a) |
| . ∩ . | set-union | f | set('a) × set('a) → set('a) |
| . ∪ . | set-union | f | set('a) × set('a) → set('a) |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | set-basic | p | set('a) × set('a) |
| . map . | set-union | f | set('a) × ('a → 'b) → set('b) |
| . to . | natset | f | nat × nat → set(nat) |
| { . } | set-union | f | 'a → set('a) |
| Σ | matrixops | f | set(nat) × (nat → ring) → ring |
| ∅ | set-basic | c | set('a) |
| I | ring | c | ring |
| O | ring | c | ring |
| O- . | ring | f | ring → ring |
| O- . | matrixops | f | matrix(ring) → matrix(ring) |
| O- . | matrixops | f | array(ring) → array(ring) |
| a | matrixops | v | ring |
| array | array | s | |
| c | matrixops | v | nat |
| disjoint | set-union | p | set('a) × set('a) |
| f | matrixops | v | nat → ring |
| filter | set-union | f | set('a) × ('a → bool) → set('a) |
| g | matrixops | v | nat × nat → ring |
| m | matrixops | v | nat |
| matrix | matrix | s | |
| mkarray | array | f | nat → array('a) |
| mkmatrix | matrix | f | nat × nat × 'a → matrix('a) |
| mx | matrixops | v | matrix(ring) |
| n | matrixops | v | nat |
| nat | nat-basic | s | |
| ns | matrixops | v | set(nat) |
| r | matrixops | v | nat |
| ring | ring | s | |
| set | set-basic | s | |
| vec | matrixops | v | array(ring) |