Bidirectional expression checking: checkExpr (Γ ⊢ e ⇓ τ) and inferExpr (Γ ⊢ e ⇑ τ), turning a CoreTLAPlus.Expression (Option TypedTLAPlus.Typ) (binder annotations still the optional, user-written ones) into a TypedTLAPlus.Expression TypedTLAPlus.Typ (every binder now a resolved type). Each case carries the rule it implements as a comment: premises over a bar over the conclusion, tagged [Rule Name].

A few constructs synthesize only in certain cases:

• ∅ is checking-only (lub over zero elements is undefined); a nonempty {e1,...,en} synthesizes Set(lub(τ1,...,τn)).
• IF/CASE are both bidirectional: each has a checking and a synthesis rule. Checked against an expected τ, every branch is checked against τ directly, so each branch picks up its own coercion from [Subtype]. In synthesis position they fall back to lub over the branches — which only succeeds when the join happens to be one of the branch types, lub being able to return only one of its two arguments (Elaborator/Subtyping.lean). Heterogeneous branches with no common branch type therefore need an expected type to flow in; that is the deliberate "require an annotation instead of implementing a real lub" trade, and the checking rules above are what make it reachable.
• ⟨e1,...,en⟩ dispatches by mode: checked against an expected Seq(τ) it uses the sequence constructor (each element checks against τ); everywhere else it synthesizes as a tuple. The elaborated term keeps the distinction (.tuple vs. .seq).
• Unbounded \A/\E synthesize only when annotated with an explicit x : τ. Unbounded CHOOSE is always checking-only — hitting it in synthesis position is a real error (TCError.cannotInferType), not a missing-annotation one. Bounded quantification/choice (x ∈ S) always synthesizes, since x's type comes from S.

Out of scope, with no CoreTLAPlus.Expression constructor to match on: LAMBDA, LET-IN, weak/strong fairness (WF_/SF_), non-stuttering ⟨A⟩_e, and temporal operators generally. UNCHANGED/ENABLED/prime '/~>/-+>/[]/<> desugar to plain operator calls, covered by the generic OPERATOR CALL rule once the builtin table gives each one a Γ entry. Only stutter ([A]_e) is a real constructor with its own case.

EXCEPT supports an arbitrary-length path of record-field/index steps per update ([f EXCEPT ![1].x[2] = v]), implemented as one general recursive walk (stepInto/checkExceptPath below) rather than one case per path length.

Polymorphism instantiation happens once, at [Var] below, not at OPERATOR CALL: a reference to a scheme Γ binding (Elaborator/Monad.lean's Binding.isScheme — a top-level operator/function definition, not an ordinary binder) freshens every distinct Typ.var in its type into its own metavariable (specializeType, Elaborator/TypeUtils.lean) right there, whether or not that reference is later called. OPERATOR CALL just checks arguments against the callee's already-specialized type, resolving those metavariables incrementally through Elaborator/Subtyping.lean's direction-aware solving.

@[reducible, inline]

abbrev SrcExpr : Type

The checker's actual input: CoreTLAPlus.Expression at α := Option Typ, every binder's annotation still the optional, user-written one rather than a resolved type.

Equations

• SrcExpr = CoreTLAPlus.Expression (Option TypedTLAPlus.Typ)

partial def indexInto {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (pos : SourceSpan) (τ : TypedTLAPlus.Typ) (idx : SrcExpr) : m (TypedTLAPlus.Typ × TypedTLAPlus.Expr)

Indexing e[e'] where e's own type τ is already known — the shared core of function call/sequence access/tuple access. CoreTLAPlus.Expression.fnCall is a single constructor covering all three, so which rule applies is a runtime dispatch on τ's own shape.

partial def stepInto {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (pos : SourceSpan) (τ : TypedTLAPlus.Typ) : String ⊕ SrcExpr → m (TypedTLAPlus.Typ × (String ⊕ TypedTLAPlus.Expr))

One EXCEPT path step (a path is a List (String ⊕ SrcExpr): .inl a record field, .inr an index) applied to an already-known type τ.

partial def checkExceptPath {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (pos : SourceSpan) (τ : TypedTLAPlus.Typ) : List (String ⊕ SrcExpr) → m (TypedTLAPlus.Typ × List (String ⊕ TypedTLAPlus.Expr))

The general EXCEPT path walk — recurses on the path, threading the type through each step via stepInto, and returns the type the final new value must be checked against alongside the elaborated (unchanged-shape) path.

partial def checkExpr {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (e : SrcExpr) (τ : TypedTLAPlus.Typ) : m TypedTLAPlus.Expr

Γ ⊢ e ⇓ τ — see the module doc for exactly which constructs get a dedicated checking rule here versus falling to the generic [Subtype] fallback (everything else, including checking-mode use of every purely-synthesis rule inferExpr implements).

partial def inferExpr {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (e : SrcExpr) : m (TypedTLAPlus.Typ × TypedTLAPlus.Expr)

Γ ⊢ e ⇑ τ — see the module doc for the precise checking/synthesis split.