structure Lean.InternalExceptionId : Type

• idx : Nat

Internal exception identifier

instance Lean.instInhabitedInternalExceptionId : Inhabited Lean.InternalExceptionId

instance Lean.instBEqInternalExceptionId : BEq Lean.InternalExceptionId

opaque Lean.internalExceptionsRef : IO.Ref (Array Lake.Name)

Internal exceptions registered in the system.

def Lean.registerInternalExceptionId (name : Lake.Name) : IO Lean.InternalExceptionId

Register a new internal exception in the system. Each internal exception has a unique index. Throw an exception if the given name is not unique. This method is usually invoked using the initialize command.

def Lean.InternalExceptionId.toString (id : Lean.InternalExceptionId) : String

Convert internal exception id into the message "internal exception #"

def Lean.InternalExceptionId.getName (id : Lean.InternalExceptionId) : IO Lake.Name

Retrieve the name used to register the internal exception.