The output of the type checker — CoreTLAPlus.Expression/Declaration/Module, every binder's annotation now a required Typ rather than optional, plus two new constructors with no CoreTLAPlus counterpart: mvar (a pending-coercion placeholder, resolved before the checker's output is ever handed to a caller) and seq (the checking-mode sequence rule, kept distinct from tuple's synthesis rule).

Most nodes don't carry a redundant "own type" field — it's recoverable from context — except where checking would otherwise need to re-synthesize it: var (the Γ-lookup result); set/seq's element type (an empty literal has no element to derive a type from); tuple's per-component types (each component can be an arbitrary expression); record/recordSet's per-field types (already present in CoreTLAPlus.Expression's shape).

@[reducible, inline]

abbrev TypedTLAPlus.Typ : Type

The type grammar, reusing SurfaceTLAPlus.Typ rather than defining a second copy: the checker's job is to populate every binder with a real value of this type, not invent a new one.

Equations

• TypedTLAPlus.Typ = SurfaceTLAPlus.Typ

@[reducible, inline]

abbrev TypedTLAPlus.MVarId : Type

The type used to identify a not-yet-resolved metavariable ?n.

Equations

• TypedTLAPlus.MVarId = ℕ

inductive TypedTLAPlus.Origin : Type

Where the name of an Expression.var node resolves, under locally-nameless binding. Carries the name (or index) itself — a .var node has no separate name field.

• bound idx — a de Bruijn index. idx counts the expression-level binders (\A/\E/CHOOSE, the two set-builders, map', fn, and operator/function parameters) enclosing the occurrence, up to and not past the one that binds it. free bindings do not count.
• free name — a Memory-keyed name: a PlusCal variable/channel/fifo, self, or a statement-level with.
• module mod name — the operator, CONSTANT, or VARIABLE name declared by module mod (own, EXTENDS-imported, or a builtinModules entry like Naturals/Sequences), resolved through Ξ/Ω.
• intrinsic name — a core-syntax builtin (=, /\, \in, \cup, DOMAIN, …) with no owning module, dispatched off the builtin table.

Baked onto Expression.var at Γ-construction time, so it survives into every downstream AST.

• bound (idx : ℕ) : Origin
• free (name : String) : Origin
• module (mod name : String) : Origin
• intrinsic (name : String) : Origin

def TypedTLAPlus.instReprOrigin.repr : Origin → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TypedTLAPlus.instReprOrigin : Repr Origin

Equations

• TypedTLAPlus.instReprOrigin = { reprPrec := TypedTLAPlus.instReprOrigin.repr }

@[implicit_reducible]

instance TypedTLAPlus.instInhabitedOrigin : Inhabited Origin

Equations

• TypedTLAPlus.instInhabitedOrigin = { default := TypedTLAPlus.instInhabitedOrigin.default }

def TypedTLAPlus.instBEqOrigin.beq : Origin → Origin → Bool

Equations

• TypedTLAPlus.instBEqOrigin.beq (TypedTLAPlus.Origin.bound a) (TypedTLAPlus.Origin.bound b) = (a == b)
• TypedTLAPlus.instBEqOrigin.beq (TypedTLAPlus.Origin.free a) (TypedTLAPlus.Origin.free b) = (a == b)
• TypedTLAPlus.instBEqOrigin.beq (TypedTLAPlus.Origin.module a a_1) (TypedTLAPlus.Origin.module b b_1) = (a == b && a_1 == b_1)
• TypedTLAPlus.instBEqOrigin.beq (TypedTLAPlus.Origin.intrinsic a) (TypedTLAPlus.Origin.intrinsic b) = (a == b)
• TypedTLAPlus.instBEqOrigin.beq x✝¹ x✝ = false

@[implicit_reducible]

instance TypedTLAPlus.instBEqOrigin : BEq Origin

Equations

• TypedTLAPlus.instBEqOrigin = { beq := TypedTLAPlus.instBEqOrigin.beq }

inductive TypedTLAPlus.Expression (α : Type) : Type

TLA⁺ expressions after type checking. α is always instantiated at Typ by the checker's actual output — kept generic to match CoreTLAPlus.Expression's own shape. Identical to CoreTLAPlus.Expression node-for-node except: var gains a trailing type (the Γ-lookup result) and an Origin; mvar/seq are new.

• 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 → α → Option (Expression α) → Expression α → Expression α

  Bounded or unbounded universal quantification.

• exists {α : Type} : String → α → Option (Expression α) → Expression α → Expression α

  Bounded or unbounded existential quantification.

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

  Temporal universal quantification \AA x : P.

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

  Temporal existential quantification.

• choose {α : Type} : String → α → Option (Expression α) → Expression α → Expression α

  Hilbert's epsilon operator.

• 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 is the bound variable's type (A's element type), cod the type of e. Both are recorded because neither recovers the other — {Len(s) : s ∈ setOfSeqs} has ann = Seq(τ) and cod = Int — and a backend needs both: Go's SetMap takes a func literal, whose signature must be written out on both sides.

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

  A function call f[e] — always unary. The head's type is recorded because f[e] is three different things depending on it (a function application, a sequence index, a tuple projection) and a backend has to tell them apart; re-deriving it means redoing inference.

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

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

• fnSet {α : Type} : Expression α → Expression α → Expression α

  The set of all functions from a domain to a codomain, [A -> B].

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

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

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

  The set of all records whose fields are in the given sets, [a : A, …, z : Z].

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

  Function update [f EXCEPT ![e] = e₂] — each path step's index is unary, same as fnCall, and like fnCall the target's type is recorded. ![i] is one syntax for overloading a function, updating a sequence and updating a tuple, which are three different operations; the path walk also needs each step's type to compile the step below it. The type of the whole expression is this same type — an override changes values, never the shape.

• 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 (fired when checking against an expected Seq(τ)) — has no CoreTLAPlus counterpart. α 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 the type of the whole conditional.

  This one is not recoverable from the branches by inspection: in synthesis position the type is lub over them, and while lub can only return one of its arguments (Elaborator/Subtyping.lean), which one is not syntactically apparent — so reading it off, say, the THEN branch is wrong whenever the join came from the ELSE. Both rules (Elaborator/Expressions.lean) coerce every branch into this type, so it is the type of each branch as elaborated, not merely an upper bound on them.

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

  Case distinction CASE p₁ -> e₁ [] … [] OTHER -> eₙ₊₁, carrying the type of the whole expression — same reasoning as if's, over lubAll of every arm.

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

  The stuttering-allowed action [A]_e.

• mvar {α : Type} : MVarId → Expression α → Expression α

  An expression-level placeholder for a pending coercion: wraps an already-elaborated expression whose true type still depends on an unresolved metavariable ?n. Has no CoreTLAPlus counterpart — every mvar node is substituted away before the checker's output is ever handed to a caller, so no consumer outside the checker itself should pattern-match on it.

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

@[implicit_reducible]

instance TypedTLAPlus.instFunctorExpression : Functor Expression

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

instance TypedTLAPlus.instTraversableExpression : Traversable Expression

Equations

• TypedTLAPlus.instTraversableExpression = { toFunctor := TypedTLAPlus.instFunctorExpression, traverse := fun {m : Type → Type} [Applicative m] {α β : Type} => TypedTLAPlus.Expression.traverse }

@[reducible, inline]

abbrev TypedTLAPlus.Declaration (α : Type) : Type

A top-level, type-checked TLA⁺ declaration. RECURSIVE and module INSTANCE are out of scope.

Equations

• TypedTLAPlus.Declaration = Declaration TypedTLAPlus.Expression

@[reducible, inline]

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

A type-checked TLA⁺ module, wrapping the (separately checked) typed PlusCal algorithm at whatever α the caller instantiates it at — kept abstract to avoid a cyclic import.

Equations

• TypedTLAPlus.Module = Module TypedTLAPlus.Expression