source
opaque Lean.exponentiation.threshold :
Lean.Option Nat
source
def Lean.checkExponent (n : Nat) (warning : Bool := true) :
CoreM Bool

Returns `true` if `n` is `≤ exponentiation.threshold`. Otherwise, reports a warning and returns `false`. This method ensures there is at most one warning message of this kind in the message log.

Equations

- One or more equations did not get rendered due to their size.

Instances For