swapBVars — Mathlib

Lean4
/-- Swaps bvars indices `i` and `j`

NOTE: the indices `i` and `j` do not correspond to the `n` in `bvar n`. Rather
they behave like indices in `Expr.lowerLooseBVars`, `Expr.liftLooseBVars`, etc.

TODO: This has to have a better implementation, but I'm still beyond confused with how bvar
indices work
-/
def _root_.Lean.Expr.swapBVars (e : Expr) (i j : Nat) : Expr :=
  let swapBVarArray : Array Expr :=
    Id.run do
      let mut a : Array Expr := .mkEmpty e.looseBVarRange
      for k in [0:e.looseBVarRange]do
        a := a.push (.bvar (if k = i then j else if k = j then i else k))
      a
  e.instantiate swapBVarArray
Похожие утверждения