Documentation

Lean.InternalExceptionId

structure Lean.InternalExceptionId:

Type

idx : Nat

instance Lean.instInhabitedInternalExceptionId:

Inhabited Lean.InternalExceptionId

Equations

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

instance Lean.instBEqInternalExceptionId:

BEq Lean.InternalExceptionId

Equations

Lean.instBEqInternalExceptionId = { beq := [anonymous] }

opaque Lean.internalExceptionsRef:

IO.Ref (Array Lean.Name)

def Lean.registerInternalExceptionId (name : Lean.Name) :

IO Lean.InternalExceptionId

Equations

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

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

Equations

Lean.InternalExceptionId.toString id = toString "internal exception #" ++ toString id.idx ++ toString ""

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

Equations

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