evalNatFib

Mathlib.Tactic.NormNum.NatFib

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

Lean4

/-- Evaluates the `Nat.fib` function. -/
@[norm_num Nat.fib _]
def evalNatFib : NormNumExt where
  eval {_ _}
    e := do
    let .app _ (x : Q(ℕ)) ← Meta.whnfR e |
      failure
    let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
    let ⟨ex, p⟩ ← deriveNat x sℕ
    let ⟨ey, pf⟩ := proveNatFib ex
    let pf' : Q(IsNat (Nat.fib $x) $ey) := q(isNat_fib $p $pf)
    return .isNat sℕ ey pf'

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

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

Разделы

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

Аффилиация

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