The desugared core syntax of TLA⁺ expressions — the output of desugaring, and the language the type checker and everything downstream actually works against.

Relative to SurfaceTLAPlus.Expression:

• @ is eliminated entirely (substituted away during desugaring).
• Conjunction/disjunction lists become binary infixCalls (.conj/.disj don't exist here).
• Every prefix/infix/postfix operator application becomes an ordinary (prefix-style) opCall, with the operator referenced by its canonical spelling through the same var constructor used for ordinary identifiers — no separate operator-enum or value constructors.
• Every quantifier-like binder (\A/\E/\AA/\EE/CHOOSE/set-map/set-filter/function literals) binds exactly one variable over at most one domain; multi-variable and tuple-pattern binders are surface sugar eliminated before reaching this type.

inductive CoreTLAPlus.Expression (α : Type) : Type

TLA⁺ expressions after desugaring. α carries whatever comment-annotation payload the binders (quantifiers, LET in the future, record fields, …) need.

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

  An unqualified identifier: a variable, a user-defined 0-ary operator, or (by canonical spelling, e.g. "+", "\\in", "DOMAIN") a builtin operator referenced as a value.

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

  An operator application f(e₁, …, eₙ) — the only form of application here, used uniformly for user-defined operators and (applying a builtin var) builtins alike.

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

  Bounded (\A x ∈ A : P, domain = some A) or unbounded (\A x : P, domain = none, the annotation α on x carrying the required explicit type) universal quantification.

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

  Bounded or unbounded existential quantification, dual to forall.

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

  Temporal universal quantification \AA x : P — always unbounded.

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

  Temporal existential quantification, dual to fforall.

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

  Hilbert's epsilon operator: bounded (CHOOSE x ∈ A : P) or unbounded (CHOOSE x : P, checked against the expected type rather than annotated).

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

  A literal set {e₁, …, eₙ}.

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

  Set filtering {x ∈ A : P}.

• map' {α : Type} : Expression α → String → α → Expression α → Expression α

  The image of a function by a set {e : x ∈ A}.

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

  A function call f[e] — always unary; a surface multi-index call f[e₁, …, eₙ] (n > 1) desugars to f[<<e₁, …, eₙ>>].

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

  A function literal [x ∈ A ↦ e].

• 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ₙ].

• 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 (.inr) is unary, same as fnCall.

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

  Record access r.x.

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

  A literal tuple <<e₁, …, eₙ>> — also TLA⁺'s only literal sequence former (Seq(S) is an ordinary opCall, not a literal).

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

  Conditional IF e₁ THEN e₂ ELSE e₃.

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

  Case distinction CASE p₁ -> e₁ [] … [] OTHER -> eₙ₊₁.

• 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.

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

@[implicit_reducible]

instance CoreTLAPlus.instFunctorExpression : Functor Expression

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

instance CoreTLAPlus.instTraversableExpression : Traversable Expression

Equations

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

@[reducible, inline]

abbrev CoreTLAPlus.Declaration (α : Type) : Type

A top-level TLA⁺ declaration. RECURSIVE and module INSTANCE are not represented.

Equations

• CoreTLAPlus.Declaration = Declaration CoreTLAPlus.Expression

@[reducible, inline]

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

A desugared TLA⁺ module, wrapping the embedded (still-Surface, not-yet-desugared-at-the- statement-level) PlusCal algorithm at whatever α the caller instantiates it at — kept abstract to avoid a cyclic import.

Equations

• CoreTLAPlus.Module = Module CoreTLAPlus.Expression