elabNormNumConv

Mathlib.Tactic.NormNum.Core

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

Lean4

/-- Elaborator for `norm_num` conv tactic. -/
@[tactic normNumConv]
def elabNormNumConv : Tactic := fun stx ↦
  withMainContext do
    let ctx ← getSimpContext stx[1] stx[3] !stx[2].isNone
    Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := true))

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

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

Разделы

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

Аффилиация

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