| 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 |
| . ( . ) | 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 |
| . ( . := . ) | 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 |
| . * . | 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 |
| . [ . ]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) |
| . exists ( . ) | set-union | p | Set('A) × ('A → Bool) |
| . filter ( . ) | set-union | f | Set[A] × (A → Bool) → Set[A] |
| . forall ( . ) | set-union | p | Set('A) × ('A → Bool) |
| . 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] |
| 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] |