Documentation

Lean.Elab.Exception

constant Lean.Elab.postponeExceptionId :

Lean.InternalExceptionId

constant Lean.Elab.unsupportedSyntaxExceptionId :

Lean.InternalExceptionId

constant Lean.Elab.abortCommandExceptionId :

Lean.InternalExceptionId

constant Lean.Elab.abortTermExceptionId :

Lean.InternalExceptionId

constant Lean.Elab.abortTacticExceptionId :

Lean.InternalExceptionId

constant Lean.Elab.autoBoundImplicitExceptionId :

Lean.InternalExceptionId

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

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

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

Option Lean.Name

Equations

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

def Lean.Elab.throwAlreadyDeclaredUniverseLevel {m : Type → Type} {α : Type} [inst : Monad m] [inst : 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} [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)

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

Equations

Lean.Elab.isAbortTacticException ex = match ex with | Lean.Exception.internal id x => id == Lean.Elab.abortTacticExceptionId | x => false

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) (msgData : Lean.MessageData) (severity : Lean.MessageSeverity) (pos : String.Pos) :

Equations

Lean.Elab.mkMessageCore fileName fileMap msgData severity pos = let pos := Lean.FileMap.toPosition fileMap pos; { fileName := fileName, pos := pos, endPos := none, severity := severity, caption := "", data := msgData }