Expand description
The operation algebra: what was done, what it asserts, how it is checked.
The operation algebra, mirrored from formal/ContextOps/Basic.lean.
Every table here is exhaustive and carries no wildcard arm. That is
deliberate: a _ arm silently absorbs a future variant, and the whole point
of this kernel is that adding an operation forces you to answer what it
asserts, how it is checked, and whether it raises depth.
Substitution — the untyped fusion of all three — is deliberately not a constructor. This kernel exists to make it unrepresentable.