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 α

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 Exception m] : m α

Equations

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

def Lean.Elab.throwIllFormedSyntax {m : Type → Type} {α : Type} [Monad m] [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 Exception m] (n : 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 : Exception) : Option 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] [MonadError m] (u : 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 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 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 Exception m] : m α

Equations

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

def Lean.Elab.isAbortTacticException (ex : 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 : 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 : FileMap) (data : MessageData) (severity : MessageSeverity) (pos endPos : String.Pos) : Message

Equations

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