renameBinderNames

Mathlib.Tactic.ToAdditive.Frontend

URI: https://scilib.ai/kg/mathlib#ToAdditive.renameBinderNames

Lean4

/-- Rename binder names in pi type. -/
def renameBinderNames (src : Expr) : Expr :=
  src.mapForallBinderNames fun
    | .str p s => .str p (guessName s)
    | n => n

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

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

Разделы

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

Аффилиация

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