def
Lean.Elab.throwPostpone
{m : Type u_1 → Type u_2}
{α : Type u_1}
[inst : 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}
[inst : MonadExceptOf Lean.Exception m]
:
m α
Equations
- Lean.Elab.throwUnsupportedSyntax = throw (Lean.Exception.internal Lean.Elab.unsupportedSyntaxExceptionId)
def
Lean.Elab.throwIllFormedSyntax
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : 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}
[inst : MonadExceptOf Lean.Exception m]
(n : Lean.Name)
:
m α
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Elab.throwAlreadyDeclaredUniverseLevel
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadError m]
(u : Lean.Name)
:
m α
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Elab.throwAbortCommand
{α : Type u_1}
{m : Type u_1 → Type u_2}
[inst : 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}
[inst : 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}
[inst : MonadExcept Lean.Exception m]
:
m α
Equations
- Lean.Elab.throwAbortTactic = throw (Lean.Exception.internal Lean.Elab.abortTacticExceptionId)
Equations
- Lean.Elab.isAbortTacticException ex = match ex with | Lean.Exception.internal id extra => id == Lean.Elab.abortTacticExceptionId | x => false
def
Lean.Elab.mkMessageCore
(fileName : String)
(fileMap : Lean.FileMap)
(data : Lean.MessageData)
(severity : Lean.MessageSeverity)
(pos : String.Pos)
(endPos : String.Pos)
:
Equations
- One or more equations did not get rendered due to their size.