opaque Lean.Elab.postponeExceptionId : InternalExceptionId

opaque Lean.Elab.unsupportedSyntaxExceptionId : InternalExceptionId

opaque Lean.Elab.abortCommandExceptionId : InternalExceptionId

opaque Lean.Elab.abortTermExceptionId : InternalExceptionId

opaque Lean.Elab.abortTacticExceptionId : InternalExceptionId

opaque Lean.Elab.autoBoundImplicitExceptionId : InternalExceptionId

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

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

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

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

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

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

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

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

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

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

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

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