The output of Typed2Computable — TypedTLAPlus.Expression restricted to what a backend can actually compute. Structurally identical to TypedTLAPlus.Expression node-for-node except:

• No fnSet ([A -> B], the set of all functions A → B) or recordSet ([a : A, ...], the set of all records shaped that way) — both denote sets with no finite representation in general, so no backend can compute them. Typed2Computable rejects any algorithm still referencing one of these (ComputableError.notComputable) rather than silently translating them into something wrong.
• No fforall/eexists (\AA/\EE, temporal quantification) or stutter ([A]_e) — already banned from anything reachable from the algorithm by WellFormedness/Restrictions.lean's check 3, so absent by construction from Typed2Computable's input; kept out of this AST entirely rather than carried forward as dead constructors no producer ever emits.
• No mvar — every metavariable is already resolved by the time the type checker's output is handed to any caller (TypedTLAPlus.Syntax.lean's doc comment), so Typed2Computable's input never contains one either.
• forall/exists/choose's domain is a required Expression α, not Option (Expression α) — WellFormedness/Restrictions.lean's check 3 already bans an unbounded quantifier (dom = none) from anything reachable from the algorithm, so every surviving domain is some by the time Typed2Computable runs; tightening the field makes that invariant checked by the type system instead of by convention.

@[reducible, inline]

abbrev ComputableTLAPlus.Typ : Type

Reuses TypedTLAPlus.Typ (itself SurfaceTLAPlus.Typ) rather than defining a third copy — Typed2Computable's job is to restrict which Expression shapes survive, not to invent a new type grammar.

Equations

• ComputableTLAPlus.Typ = TypedTLAPlus.Typ

@[reducible, inline]

abbrev ComputableTLAPlus.Origin : Type

Reuses TypedTLAPlus.Origin — a .var's provenance doesn't change across Typed2Computable, only which expressions are allowed to exist at all.

Equations

• ComputableTLAPlus.Origin = TypedTLAPlus.Origin

inductive ComputableTLAPlus.Expression (α : Type) : Type

Computable TLA⁺ expressions — see the module doc above for how this differs from TypedTLAPlus.Expression. α is always instantiated at Typ by Typed2Computable's output — kept generic to match TypedTLAPlus.Expression's shape.

• var {α : Type} : α → Origin → Expression α

  An identifier: its type resolved via Γ and its Origin recording where the name binds. A .bound node carries no name — the string hint lives on the enclosing binder.

• opCall {α : Type} : Expression α → List (Expression α) → Expression α

  An operator application f(e₁, …, eₙ).

• forall {α : Type} : String → α → Expression α → Expression α → Expression α

  Bounded universal quantification.

• exists {α : Type} : String → α → Expression α → Expression α → Expression α

  Bounded existential quantification.

• choose {α : Type} : String → α → Expression α → Expression α → Expression α

  Hilbert's epsilon operator, bounded.

• set {α : Type} : List (Expression α) → α → Expression α

  A literal set {e₁, …, eₙ}, α its element type — kept since an empty {} gives nothing to reconstruct it from.

• collect {α : Type} : String → α → Expression α → Expression α → Expression α

  Set filtering {x ∈ A : P}.

• map' {α : Type} : Expression α → String → (ann cod : α) → Expression α → Expression α

  The image of a function by a set {e : x ∈ A}. ann/cod as in TypedTLAPlus.Expression.map'.

• fnCall {α : Type} : Expression α → (fnTyp : α) → Expression α → Expression α

  A function call f[e] — always unary, carrying its head's type so that a backend can tell a function application from a sequence index from a tuple projection.

• fn {α : Type} : String → (ann cod : α) → Expression α → Expression α → Expression α

  A function literal [x ∈ A ↦ e]. ann/cod as in map'.

• record {α : Type} : List (α × String × Expression α) → Expression α

  A literal record [a |-> e₁, …, z |-> eₙ], each field's own α its (ascribed or inferred) type.

• except {α : Type} : Expression α → (τ : α) → List (List (String ⊕ Expression α) × Expression α) → Expression α

  Function update [f EXCEPT ![e] = e₂], carrying the target's type — see TypedTLAPlus.Expression.except.

• recordAccess {α : Type} : Expression α → String → Expression α

  Record access r.x.

• tuple {α : Type} : List (α × Expression α) → Expression α

  A literal tuple <<e₁, …, eₙ>>, synthesis-mode. Each component pairs its own type with itself directly, since a component's type isn't a cheap pattern-match away in general. Kept distinct from seq below — the same surface syntax, but a different elaboration rule.

• seq {α : Type} : List (Expression α) → α → Expression α

  A literal sequence <<e₁, …, eₙ>>, checking-mode only. α the element type τ every eᵢ was checked against — kept because an empty <<>> gives nothing to reconstruct it from.

• if {α : Type} : Expression α → Expression α → Expression α → (τ : α) → Expression α

  Conditional IF e₁ THEN e₂ ELSE e₃, carrying its own type — see TypedTLAPlus.Expression.if for why no branch answers for it.

• case {α : Type} : List (Expression α × Expression α) → Option (Expression α) → (τ : α) → Expression α

  Case distinction CASE p₁ -> e₁ [] … [] OTHER -> eₙ₊₁, carrying its own type.

• nat {α : Type} : String → Expression α
• str {α : Type} : String → Expression α
• true {α : Type} : Expression α
• false {α : Type} : Expression α

@[implicit_reducible]

instance ComputableTLAPlus.instReprExpression {α✝ : Type} [Repr α✝] : Repr (Expression α✝)

Equations

• ComputableTLAPlus.instReprExpression = { reprPrec := ComputableTLAPlus.instReprExpression.repr }

partial def ComputableTLAPlus.instReprExpression.repr {α✝ : Type} [Repr α✝] : Expression α✝ → ℕ → Std.Format

@[implicit_reducible]

instance ComputableTLAPlus.instInhabitedExpression {a✝ : Type} : Inhabited (Expression a✝)

Equations

• ComputableTLAPlus.instInhabitedExpression = { default := ComputableTLAPlus.instInhabitedExpression.default }

@[implicit_reducible]

instance ComputableTLAPlus.instBEqExpression {α✝ : Type} [BEq α✝] : BEq (Expression α✝)

Equations

• ComputableTLAPlus.instBEqExpression = { beq := ComputableTLAPlus.instBEqExpression.beq }

partial def ComputableTLAPlus.instBEqExpression.beq {α✝ : Type} [BEq α✝] : Expression α✝ → Expression α✝ → Bool

partial def ComputableTLAPlus.Expression.map {α β : Type} (f : α → β) (e : Expression α) : Expression β

@[implicit_reducible]

instance ComputableTLAPlus.instFunctorExpression : Functor Expression

Equations

• ComputableTLAPlus.instFunctorExpression = { map := fun {α β : Type} => ComputableTLAPlus.Expression.map }

@[implicit_reducible]

def ComputableTLAPlus.instInhabitedExpressionOfApplicative {F : Type → Type} [Applicative F] {α : Type} : Inhabited (F (Expression α))

Equations

• ComputableTLAPlus.instInhabitedExpressionOfApplicative = { default := pure ComputableTLAPlus.Expression.true }

partial def ComputableTLAPlus.Expression.traverse {F : Type → Type} [Applicative F] {α β : Type} (f : α → F β) (e : Expression α) : F (Expression β)

@[implicit_reducible]

instance ComputableTLAPlus.instTraversableExpression : Traversable Expression

Equations

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

@[reducible, inline]

abbrev ComputableTLAPlus.Declaration (α : Type) : Type

A top-level, computable TLA⁺ declaration.

Equations

• ComputableTLAPlus.Declaration = Declaration ComputableTLAPlus.Expression

@[reducible, inline]

abbrev ComputableTLAPlus.Module (α β : Type) : Type

A computable TLA⁺ module, wrapping the (separately translated) ComputablePlusCal algorithm at whatever α the caller instantiates it at — kept abstract to avoid a cyclic import, same as TypedTLAPlus.Module.

Equations

• ComputableTLAPlus.Module = Module ComputableTLAPlus.Expression