Documentation

Lean.Elab.Exception

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 : Lake.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 Lake.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 : Lake.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) :

Equations

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

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) :

Equations

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