opaque Lean.Elab.postponeExceptionId : Lean.InternalExceptionId

opaque Lean.Elab.unsupportedSyntaxExceptionId : Lean.InternalExceptionId

opaque Lean.Elab.abortCommandExceptionId : Lean.InternalExceptionId

opaque Lean.Elab.abortTermExceptionId : Lean.InternalExceptionId

opaque Lean.Elab.abortTacticExceptionId : Lean.InternalExceptionId

opaque Lean.Elab.autoBoundImplicitExceptionId : Lean.InternalExceptionId

def Lean.Elab.throwPostpone {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Lean.Exception m] : m α

Equations

• Lean.Elab.throwPostpone = throw (Lean.Exception.internal Lean.Elab.postponeExceptionId)

def Lean.Elab.throwUnsupportedSyntax {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Lean.Exception m] : m α

Equations

• Lean.Elab.throwUnsupportedSyntax = throw (Lean.Exception.internal Lean.Elab.unsupportedSyntaxExceptionId)

def Lean.Elab.throwIllFormedSyntax {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] : m α

Equations

• Lean.Elab.throwIllFormedSyntax = Lean.throwError (Lean.toMessageData "ill-formed syntax")

def Lean.Elab.throwAutoBoundImplicitLocal {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Lean.Exception m] (n : Lean.Name) : m α

Equations

• Lean.Elab.throwAutoBoundImplicitLocal n = throw (Lean.Exception.internal Lean.Elab.autoBoundImplicitExceptionId (Lean.KVMap.empty.insert `localId (Lean.DataValue.ofName n)))

def Lean.Elab.isAutoBoundImplicitLocalException? (ex : Lean.Exception) : Option Lean.Name

Equations

• Lean.Elab.isAutoBoundImplicitLocalException? (Lean.Exception.internal id k) = if (id == Lean.Elab.autoBoundImplicitExceptionId) = true then some (k.getName `localId `x) else none
• Lean.Elab.isAutoBoundImplicitLocalException? ex = none

def Lean.Elab.throwAlreadyDeclaredUniverseLevel {m : Type → Type} {α : Type} [Monad m] [Lean.MonadError m] (u : Lean.Name) : m α

Equations

• Lean.Elab.throwAlreadyDeclaredUniverseLevel u = Lean.throwError (Lean.toMessageData "a universe level named '" ++ Lean.toMessageData u ++ Lean.toMessageData "' has already been declared")

def Lean.Elab.throwAbortCommand {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] : m α

Equations

• Lean.Elab.throwAbortCommand = throw (Lean.Exception.internal Lean.Elab.abortCommandExceptionId)

def Lean.Elab.throwAbortTerm {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] : m α

Equations

• Lean.Elab.throwAbortTerm = throw (Lean.Exception.internal Lean.Elab.abortTermExceptionId)

def Lean.Elab.throwAbortTactic {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] : m α

Equations

• Lean.Elab.throwAbortTactic = throw (Lean.Exception.internal Lean.Elab.abortTacticExceptionId)

def Lean.Elab.isAbortTacticException (ex : Lean.Exception) : Bool

Equations

• Lean.Elab.isAbortTacticException (Lean.Exception.internal id k) = (id == Lean.Elab.abortTacticExceptionId)
• Lean.Elab.isAbortTacticException ex = false

def Lean.Elab.isAbortExceptionId (id : Lean.InternalExceptionId) : Bool

Equations

• Lean.Elab.isAbortExceptionId id = (id == Lean.Elab.abortCommandExceptionId || id == Lean.Elab.abortTermExceptionId || id == Lean.Elab.abortTacticExceptionId)

def Lean.Elab.mkMessageCore (fileName : String) (fileMap : Lean.FileMap) (data : Lean.MessageData) (severity : Lean.MessageSeverity) (pos : String.Pos) (endPos : String.Pos) : Lean.Message

Equations

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