@[extern lean_closure_max_args]

opaque Lean.closureMaxArgsFn : Unit → Nat

@[extern lean_max_small_nat]

opaque Lean.maxSmallNatFn : Unit → Nat

def Lean.closureMaxArgs : Nat

Equations

• Lean.closureMaxArgs = Lean.closureMaxArgsFn ()

def Lean.maxSmallNat : Nat

Equations

• Lean.maxSmallNat = Lean.maxSmallNatFn ()