structure Lean.InternalExceptionId : Type

Internal exception identifier

• idx : Nat

instance Lean.instInhabitedInternalExceptionId : Inhabited InternalExceptionId

instance Lean.instBEqInternalExceptionId : BEq InternalExceptionId

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

Internal exceptions registered in the system.

def Lean.registerInternalExceptionId (name : Name) : IO 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 : InternalExceptionId) : String

Convert internal exception id into the message "internal exception #<idx>"

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

Retrieve the name used to register the internal exception.