applyReplacementForall — Mathlib

Lean4
/-- Run `applyReplacementFun` on an expression `∀ x₁ .. xₙ, e`,
making sure not to translate type-classes on `xᵢ` if `i` is in `dontTranslate`. -/
def applyReplacementForall (dontTranslate : List Nat) (e : Expr) : MetaM Expr := do
  if let some maxDont := dontTranslate.max? then
    forallBoundedTelescope e (some (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 := .forallE decl.userName xType (e.abstract #[.fvar x]) decl.binderInfo
        return e
  else
    applyReplacementFun e #[]
Похожие утверждения