The effects the type checker needs: a local typing context Γ, a metavariable context, error reporting, and fresh-name generation.

structure Binding : Type

One Γ entry in the named half of Context (below): a Memory-keyed name (Origin.free — PlusCal variables/channels/fifos, self) or a top-level declaration (Origin.module/Origin.intrinsic — CONSTANT/VARIABLE/operator/function/builtin). type is the Γ-lookup result; isScheme marks a declaration whose Typ.vars are freshened into fresh metavariables at every reference (specializeType, Elaborator/Expressions.lean's inferExpr) — only operator/function definitions and builtinContext entries; and origin is the Origin baked onto every Expression.var node that resolves here. Expression-level lexical binders (\A/\E/CHOOSE/set-builders/map'/fn, operator/function parameters) are not Bindings — they live on Context.lexical as de Bruijn positions. No default for origin — every construction site says which.

• type : TypedTLAPlus.Typ
• isScheme : Bool
• origin : TypedTLAPlus.Origin

structure Context : Type

The local typing context Γ, split by how a name resolves under locally-nameless binding:

• lexical — expression-level binders, innermost first. A .var reference matching entry i here elaborates to Origin.bound i.
• named — everything Memory-keyed or top-level (Origin.free/.module/.intrinsic), each carrying its own Binding. A .var match here takes the stored origin verbatim.

lexical is consulted first, so an expression binder shadows a same-named PlusCal variable for the scope of its body.

• lexical : List (String × TypedTLAPlus.Typ)
• named : Std.HashMap String Binding

class MonadMetavarContext (α : outParam Type) (m : Type → Type) : Type

The metavariable context: tracks only whether each metavariable is resolved, and to what. MVarId is fixed at this project's own TypedTLAPlus.MVarId (:= Nat).

The pending-upper-bounds bookkeeping the direction-aware solving algorithm needs on top of this is Elaborator/Subtyping.lean's job to layer over this class, not this file's concern.

• mkFreshMVar : m TypedTLAPlus.MVarId

  Allocate a new, as-yet-unresolved metavariable.

• assignMVar : TypedTLAPlus.MVarId → α → m Unit

  Resolve a metavariable to a concrete value. A no-op if already resolved.

• assigned? : TypedTLAPlus.MVarId → m (Option α)

  The metavariable's resolved value, if any.

structure MetavarContext (α : Type) : Type

Backing store for the generic MonadMetavarContext instance below: index n holds ?n's resolved value, or none while still unresolved.

• mvars : Array (Option α)

@[implicit_reducible]

instance instEmptyCollectionMetavarContext {α : Type} : EmptyCollection (MetavarContext α)

Equations

• instEmptyCollectionMetavarContext = { emptyCollection := { mvars := #[] } }

@[implicit_reducible]

instance instMonadMetavarContextOfMonadOfInhabitedOfMonadStateOfMetavarContext {α : Type} {m : Type → Type} [Monad m] [Inhabited α] [MonadStateOf (MetavarContext α) m] : MonadMetavarContext α m

Equations

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

class MonadElaborator (m : Type → Type) extends MonadReaderOf Context m, MonadWithReaderOf Context m, MonadMetavarContext TypedTLAPlus.Typ m, MonadDiagnostic TCWarning TCError m, MonadFresh m : Type 1

The effect bundle the checker's expression/declaration/PlusCal-level rules check against.

• read : m Context
• withReader {α : Type} (f : Context → Context) (x : m α) : m α
• mkFreshMVar : m TypedTLAPlus.MVarId
• assignMVar : TypedTLAPlus.MVarId → TypedTLAPlus.Typ → m Unit
• assigned? : TypedTLAPlus.MVarId → m (Option TypedTLAPlus.Typ)
• tell (w : List TCWarning) : m PUnit.{1}
• listen {α : Type} (f : m α) : m (α × List TCWarning)
• pass {α : Type} (f : m (α × (List TCWarning → List TCWarning))) : m α
• throw {α : Type} : TCError → m α
• tryCatch {α : Type} (body : m α) (handler : TCError → m α) : m α
• fresh : m ℕ