| 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 |
| . .filter ( . ) | set-union | f | Set('a) × ('a → Bool) → Set('a) |
| . .map ( . ) | set-union | f | Set('a) × ('a → 'b) → Set('b) |
| . < . | 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) |
| . 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) |
| Array | array | s | |
| I | ring | c | Ring |
| Matrix | matrix | s | |
| Nat | nat-basic | s | |
| O | ring | c | Ring |
| O- . | ring | f | Ring → Ring |
| O- . | matrixops | f | Matrix(Ring) → Matrix(Ring) |
| O- . | matrixops | f | Array(Ring) → Array(Ring) |
| Ring | ring | s | |
| Set | set-basic | s | |
| a | matrixops | v | Ring |
| c | matrixops | v | Nat |
| disjoint | set-union | p | Set('a) × Set('a) |
| f | matrixops | v | Nat → Ring |
| g | matrixops | v | Nat × Nat → Ring |
| m | matrixops | v | Nat |
| mkarray | array | f | Nat → Array('a) |
| mkarray | array | f | Nat × 'a → Array('a) |
| mkmatrix | matrix | f | Nat × Nat × 'a → Matrix('a) |
| mx | matrixops | v | Matrix(Ring) |
| n | matrixops | v | Nat |
| ns | matrixops | v | Set(Nat) |
| r | matrixops | v | Nat |
| vec | matrixops | v | Array(Ring) |