structure Lean.InternalExceptionId : Type

Internal exception identifier

• idx : Nat

instance Lean.instInhabitedInternalExceptionId : Inhabited Lean.InternalExceptionId

Equations

• Lean.instInhabitedInternalExceptionId = { default := { idx := default } }

instance Lean.instBEqInternalExceptionId : BEq Lean.InternalExceptionId

Equations

• Lean.instBEqInternalExceptionId = { beq := Lean.beqInternalExceptionId✝ }

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.

Equations

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

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

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

Equations

• id.toString = toString "internal exception #" ++ toString id.idx ++ toString ""

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

Retrieve the name used to register the internal exception.

Equations

• id.getName = do let exs ← ST.Ref.get Lean.internalExceptionsRef let i : Nat := id.idx if h : i < exs.size then pure (exs.get ⟨i, h⟩) else throw (IO.userError "invalid internal exception id")