evalNatSqrt

Mathlib.Tactic.NormNum.NatSqrt

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.evalNatSqrt

Lean4

/-- Evaluates the `Nat.sqrt` function. -/
@[norm_num Nat.sqrt _]
def evalNatSqrt : 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⟩ := proveNatSqrt ex
    let pf' : Q(IsNat (Nat.sqrt $x) $ey) := q(isNat_sqrt $p $pf)
    return .isNat sℕ ey pf'

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

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

Разделы

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

Аффилиация

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