applyReplacementLambda — Mathlib

Lean4
/-- Run `applyReplacementFun` on an expression `fun x₁ .. xₙ ↦ e`,
making sure not to translate type-classes on `xᵢ` if `i` is in `dontTranslate`. -/
def applyReplacementLambda (dontTranslate : List Nat) (e : Expr) : MetaM Expr := do
  if let some maxDont := dontTranslate.max? then
    lambdaBoundedTelescope e (maxDont + 1) fun xs e => do
        let xs := xs.map (·.fvarId!)
        let dontTranslate := dontTranslate.filterMap (xs[·]?) |>.toArray
        let mut e ← applyReplacementFun e dontTranslate
        for x in xs.reverse do
          let decl ← x.getDecl
          let xType ← applyReplacementFun decl.type dontTranslate
          e := .lam decl.userName xType (e.abstract #[.fvar x]) decl.binderInfo
        return e
  else
    applyReplacementFun e #[]
Похожие утверждения