clean

Mathlib.Tactic.Clean

URI: https://scilib.ai/kg/mathlib#Lean.Expr.clean

Lean4

/-- Clean an expression by eliminating identify functions listed in `cleanConsts`.
Also eliminates `fun x => x` applications and tautological `let`/`have` bindings. -/
def clean (e : Expr) : Expr :=
  e.replace fun
    | .app (.app (.const n _) _) e' => if n ∈ cleanConsts then some e' else none
    | .app (.lam _ _ (.bvar 0) _) e' => some e'
    | .letE _ _ v (.bvar 0) _ => some v
    | _ => none

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

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

Разделы

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

Аффилиация

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