zetaDelta

Mathlib.Tactic.DepRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.DepRewrite.zetaDelta

Lean4

/-- In `e`, inline the values of those `ldecl`s that appear in `fvars`. -/
def zetaDelta (e : Expr) (fvars : Std.HashSet FVarId) : MetaM Expr :=
  let unfold? (fvarId : FVarId) : MetaM (Option Expr) := do
    if fvars.contains fvarId then
      fvarId.getValue?
    else
      return none
  let pre (e : Expr) : MetaM TransformStep := do
    let .fvar fvarId := e |
      return .continue
    let some val ← unfold? fvarId |
      return .continue
    return .visit val
  transform e (pre := pre)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru