Declaration/module-level checking: checkDeclaration/checkDeclarations, threading Γ across CONSTANTS/VARIABLES/ASSUME/operator-definition/function-definition, plus builtinContext, a minimal Γ₀ prelude of core TLA⁺ operators (equality, boolean connectives, core set theory) needed before any user declaration is checked.

Every declaration's expressions are closed out via resolveMVars before checkDeclaration returns, so a metavariable freshened during one declaration doesn't leak unresolved into the next declaration's Γ.

THEOREM/RECURSIVE are out of scope: neither has a CoreTLAPlus.Declaration constructor. Operator definitions thus get no self- or mutual recursion (their own name is never in scope for their own body); function definitions get self-recursion unconditionally (f is in scope checking its own body), matching ordinary TLA⁺ recursive functions.

A multi-argument function definition f[x₁ ∈ e₁,...,xₙ ∈ eₙ] isn't pre-tupled the way a multi-index call is: n = 1 gives a domain type of τ₁ itself; n > 1 requires the annotation's domain to be Typ.tuple [τ₁,...,τₙ].

@[reducible, inline]

abbrev SrcDecl : Type

The checker's actual input for one declaration: CoreTLAPlus.Declaration at α := Option Typ.

Equations

• SrcDecl = CoreTLAPlus.Declaration (Option TypedTLAPlus.Typ)

@[reducible, inline]

abbrev Decl : Type

The checker's output for one declaration.

Equations

• Decl = TypedTLAPlus.Declaration TypedTLAPlus.Typ

def builtinContext : Context

Γ₀ — the minimal builtin prelude. Every entry is a scheme (Binding.isScheme := true): each is a genuine operator definition, so Typ.vars used for whatever's meant to be generic get freshened into their own metavariable at every reference (specializeType, Elaborator/Expressions.lean's inferExpr).

Equations

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

def checkDeclaration {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (moduleName : String) (d : SrcDecl) : m (Decl × List (String × Binding))

Γ ⊢ D ⊣ Γ' — checks one declaration, returning its elaborated form alongside the bindings Γ' adds over Γ ([] for ASSUME, which adds none). A CONSTANT/VARIABLE binding is never a scheme (Binding.isScheme := false, even if its annotation mentions a Typ.var): a CONSTANT is one fixed, if abstract, value, not a family to instantiate fresh per reference. An operator/function definition's own binding is a scheme, any arity — see each case below.

Equations

• One or more equations did not get rendered due to their size.
• checkDeclaration moduleName (Declaration.assume e) = do let e' ← checkExpr e SurfaceTLAPlus.Typ.bool let e' ← resolveMVars e' pure (Declaration.assume e', [])

def checkDeclarations {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (moduleName : String) : List SrcDecl → m (List Decl × List (String × Binding))

Γ ⊢ D₁, …, Dₙ ⊣ Γ' — checks a whole declaration list, threading Γ through each one. Returns the accumulated Γ' \ Γ bindings alongside the checked declarations.

Equations

• One or more equations did not get rendered due to their size.
• checkDeclarations moduleName [] = pure ([], [])