def Context.lookup (ctx : Context) (x : String) : Option (TypedTLAPlus.Typ × TypedTLAPlus.Origin × Bool)

Resolve x against Γ: lexical first (an expression binder at position i → Origin.bound i), then named (a Memory-keyed name or a declaration, taking its stored Origin). Returns the type, the Origin to bake onto the .var node, and whether the binding is a scheme.

Equations

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

def Context.insertNamed (ctx : Context) (x : String) (b : Binding) : Context

Insert one already-tagged named binding — used to build the initial Γ from a module's imports (Driver/Modules.lean).

Equations

• ctx.insertNamed x b = { lexical := ctx.lexical, named := ctx.named.insert x b }

def extend {m : Type → Type} [MonadElaborator m] {α : Type} (x : String) (τ : TypedTLAPlus.Typ) (act : m α) : m α

Push one expression-level lexical binder for the scope of act — a quantifier, CHOOSE, set-builder, map'/fn, EXCEPT binder, or multicast filter recipient. References to x inside act elaborate to Origin.bound 0 at the top of the pushed scope.

Equations

• extend x τ act = withTheReader Context (fun (c : Context) => { lexical := (x, τ) :: c.lexical, named := c.named }) act

def extendAll {m : Type → Type} [MonadElaborator m] {α : Type} (bindings : List (String × TypedTLAPlus.Typ)) (act : m α) : m α

Push several lexical binders at once — operator/function parameters. bindings is in declaration order (Op(a, b) ⇒ [(a, _), (b, _)]), so the last parameter ends up innermost: a elaborates to Origin.bound 1, b to Origin.bound 0.

Equations

• extendAll bindings act = withTheReader Context (fun (c : Context) => { lexical := bindings.reverse ++ c.lexical, named := c.named }) act

def extendFree {m : Type → Type} [MonadElaborator m] {α : Type} (x : String) (τ : TypedTLAPlus.Typ) (act : m α) : m α

Add one Memory-keyed name (Origin.free — a PlusCal variable/channel/fifo, self, or a statement-level with) for the scope of act.

Equations

• extendFree x τ act = withTheReader Context (fun (c : Context) => { lexical := c.lexical, named := c.named.insert x { type := τ, origin := TypedTLAPlus.Origin.free x } }) act

def extendAllFree {m : Type → Type} [MonadElaborator m] {α : Type} (bindings : List (String × TypedTLAPlus.Typ)) (act : m α) : m α

extendFree over a list — a whole variables/channels/fifos block, or a process's local state in scope for its threads.

Equations

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

def extendAllBindings {m : Type → Type} [MonadElaborator m] {α : Type} (bindings : List (String × Binding)) (act : m α) : m α

Extend Γ with a list of already-tagged named Bindings (each carrying its own isScheme/origin) for the scope of act — a checked declaration list's operator/function schemes and CONSTANT/VARIABLE bindings.

Equations

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

def requireAnnotation {m : Type → Type} [Monad m] [MonadElaborator m] (pos : SourceSpan) (what : String) : Option TypedTLAPlus.Typ → m TypedTLAPlus.Typ

Requires that an annotation be present, erroring at pos with what otherwise.

Equations

• requireAnnotation pos what (some τ) = pure τ
• requireAnnotation pos what none = throw (TCError.expectedTypeAnnotation pos what)