Documentation

Mathlib.Tactic.NormNum.NatLog

norm_num extension for Nat.log #

This module defines a norm_num extension for Nat.log.

source
def Mathlib.Meta.NormNum.proveNatLog (eb en : Q(ℕ)) :
(ek : Q(ℕ)) × Q(Nat.log «$eb» «$en» = «$ek»)

Given the natural number literals eb and en, returns Nat.log eb en as a natural number literal and an equality proof. Panics if ex or en aren't natural number literals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Meta.NormNum.evalNatLog :
    NormNumExt

    Evaluates the Nat.log function.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For