elabNormNum1Conv

Mathlib.Tactic.NormNum.Core

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

Lean4

/-- Elaborator for `norm_num1` conv tactic. -/
@[tactic normNum1Conv]
def elabNormNum1Conv : Tactic := fun _ ↦
  withMainContext do
    let ctx ← getSimpContext mkNullNode mkNullNode true
    Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := false))

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

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

Разделы

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

Аффилиация

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