De Bruijn index manipulation for TypedTLAPlus.Expression under locally-nameless binding.

Origin.bound uses standard de Bruijn indices: .bound 0 is the nearest enclosing expression-level binder (\A/\E/CHOOSE, the two set-builders, map', fn, and operator/function parameters). Origin.free names live in a separate namespace and never move an index.

liftBound (shift the free .bound indices), openVar (a binder body's reference to its own binder becomes a free name) and close (its inverse) are one depth-tracking traversal, mapVars.

partial def TypedTLAPlus.Expression.mapVars {α : Type} (f : ℕ → α → Origin → SourceSpan → Expression α) (k : ℕ) (e : Expression α) : Expression α

Rebuild every .var node knowing the number of expression-level binders enclosing it: f k τ o pos is the replacement for a .var τ o sitting at binder depth k. Each binder arm recurses into its scoped body at k + 1; domain and annotation positions stay at k.

def TypedTLAPlus.Expression.liftBound {α : Type} (d : ℕ) (e : Expression α) : Expression α

Add d to every .bound index that refers past e's own binders.

Equations

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

def TypedTLAPlus.Expression.openVar {α : Type} (name : String) (e : Expression α) : Expression α

In a binder's body — already stripped of that binder — turn the reference to the removed binder into the free name name, and shift every deeper free index down by one.

Equations

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

def TypedTLAPlus.Expression.close {α : Type} (name : String) (e : Expression α) : Expression α

Bind every free occurrence of name as a new outermost .bound, shifting every deeper free index up by one. Inverse of openVar.

Equations

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