evalNatClog

Mathlib.Tactic.NormNum.NatLog

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.evalNatClog

Lean4

/-- Evaluates the `Nat.clog` function.
-/
@[norm_num Nat.clog _ _]
def evalNatClog : NormNumExt where
  eval {u α}
    e := do
    let mkApp2 _ (b : Q(ℕ)) (n : Q(ℕ)) ← Meta.whnfR e |
      failure
    let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
    let ⟨eb, pb⟩ ← deriveNat b sℕ
    let ⟨en, pn⟩ ← deriveNat n sℕ
    let ⟨ek, pf⟩ := proveNatClog eb en
    let pf' : Q(IsNat (Nat.clog $b $n) $ek) := q(isNat_clog $pb $pn $pf)
    return .isNat sℕ ek pf'

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

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

Разделы

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

Аффилиация

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