structure Lean.InternalExceptionId : Type

Internal exception identifier

• idx : Nat

Instances For

• Lean.instBEqInternalExceptionId
• Lean.instInhabitedInternalExceptionId

instance Lean.instInhabitedInternalExceptionId : Inhabited InternalExceptionId

Equations

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

instance Lean.instBEqInternalExceptionId : BEq InternalExceptionId

Equations

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

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.

Equations

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

def Lean.InternalExceptionId.toString (id : 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 : InternalExceptionId) : IO 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[i] else throw (IO.userError "invalid internal exception id")