refoldFVars — Mathlib

Lean4
/-- For each fvar, looks for its body in `e` and replaces it with the fvar. -/
def refoldFVars (fvars : Array FVarId) (loc? : Option FVarId) (e : Expr) : MetaM Expr := do
  -- Filter the fvars, only taking those that are from earlier in the local context.

  let fvars ←
    if let some loc := loc? then
      let locIndex := (← loc.getDecl).index
      fvars.filterM fun fvar => do
          let some decl ← fvar.findDecl? |
            return false
          return decl.index < locIndex
    else
      pure fvars
  let mut e := e
  for fvar in fvars do
    let some val ← fvar.getValue? |
      throwError "local variable {Expr.fvar fvar} has no value to refold"
    e := (← kabstract e val).instantiate1 (Expr.fvar fvar)
  return e
Похожие утверждения