addLocalRewriteEntry

Mathlib.Tactic.Widget.LibraryRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LibraryRewrite.addLocalRewriteEntry

Lean4

/-- Try adding the local hypothesis to the `RefinedDiscrTree`. -/
def addLocalRewriteEntry (decl : LocalDecl) : MetaM (List ((FVarId × Bool) × List (Key × LazyEntry))) :=
  withReducible
    (do
      let (_, _, eqn) ← forallMetaTelescope decl.type
      let some (lhs, rhs) := eqOrIff? eqn |
        return []
      let result := ((decl.fvarId, false), ← initializeLazyEntryWithEta lhs)
      return [result, ((decl.fvarId, true), ← initializeLazyEntryWithEta rhs)])

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

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

Разделы

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

Аффилиация

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