Typed2Computable's diagnostics — one named error variant per genuinely new restriction this pass introduces beyond WellFormedness, plus a defense-in-depth catch-all for inputs that should be unreachable by construction.

inductive NonComputableConstruct : Type

Which non-computable construct ComputableError.notComputable reports — the two TypedTLAPlus.Expression constructors Core/ComputableTLAPlus/Syntax.lean has no counterpart for: fnSet ([A -> B], the set of all functions from A to B) and recordSet ([a : A, ...], the set of all records shaped that way) — both denote sets with no finite runtime representation.

• fnSet : NonComputableConstruct

  [A -> B], the set of all functions from A to B.

• recordSet : NonComputableConstruct

  [a : A, ...], the set of all records shaped that way.

@[implicit_reducible]

instance instReprNonComputableConstruct : Repr NonComputableConstruct

Equations

• instReprNonComputableConstruct = { reprPrec := instReprNonComputableConstruct.repr }

def instReprNonComputableConstruct.repr : NonComputableConstruct → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instInhabitedNonComputableConstruct : Inhabited NonComputableConstruct

Equations

• instInhabitedNonComputableConstruct = { default := instInhabitedNonComputableConstruct.default }

def instBEqNonComputableConstruct.beq : NonComputableConstruct → NonComputableConstruct → Bool

Equations

• instBEqNonComputableConstruct.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance instBEqNonComputableConstruct : BEq NonComputableConstruct

Equations

• instBEqNonComputableConstruct = { beq := instBEqNonComputableConstruct.beq }

inductive ComputableError : Type

Typed2Computable's errors.

• notComputable (pos : SourceSpan) (construct : NonComputableConstruct) : ComputableError

  The algorithm references fnSet/recordSet — genuinely not computable under this compiler's finite-sets assumption, and not enforced by WellFormedness (whose checks ban temporal/action operators and unbounded quantifiers, not these).

• internalInvariantViolated (pos : SourceSpan) (description : String) : ComputableError

  Defense-in-depth: a construct WellFormedness/Restrictions.lean's check 3 already guarantees can't be transitively-reachable-from-the-algorithm (an unbounded forall/exists/ choose domain, or a bare fforall/eexists/stutter) still turned up, or a pending coercion (mvar) survived past the type checker's own output despite Core/TypedTLAPlus/ Syntax.lean's own guarantee that none do. No proof of unreachability exists for any of these yet — just facts established by earlier passes — so this stays a runtime check, not absurd/nomatch.

@[implicit_reducible]

instance instReprComputableError : Repr ComputableError

Equations

• instReprComputableError = { reprPrec := instReprComputableError.repr }

def instReprComputableError.repr : ComputableError → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instInhabitedComputableError : Inhabited ComputableError

Equations

• instInhabitedComputableError = { default := instInhabitedComputableError.default }

@[implicit_reducible]

instance instBEqComputableError : BEq ComputableError

Equations

• instBEqComputableError = { beq := instBEqComputableError.beq }

def instBEqComputableError.beq : ComputableError → ComputableError → Bool

Equations

• instBEqComputableError.beq (ComputableError.notComputable a a_1) (ComputableError.notComputable b b_1) = (a == b && a_1 == b_1)
• instBEqComputableError.beq (ComputableError.internalInvariantViolated a a_1) (ComputableError.internalInvariantViolated b b_1) = (a == b && a_1 == b_1)
• instBEqComputableError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instCompilerDiagnosticComputableErrorString : CompilerDiagnostic ComputableError String

Equations

• One or more equations did not get rendered due to their size.