opaque Lean.exponentiation.threshold : Lean.Option Nat

def Lean.checkExponent (n : Nat) : 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.