Documentation

Lean.Exception

inductive Lean.Exception :

Type

error: Lean.Syntax → Lean.MessageData → Lean.Exception
internal: Lean.InternalExceptionId → optParam Lean.KVMap { entries := [] } → Lean.Exception

def Lean.Exception.toMessageData :

Lean.Exception → Lean.MessageData

Equations

Lean.Exception.toMessageData x = match x with | Lean.Exception.error x msg => msg | Lean.Exception.internal id x => Function.comp Lean.MessageData.ofFormat Lean.format (Lean.InternalExceptionId.toString id)

def Lean.Exception.getRef :

Lean.Exception → Lean.Syntax

Equations

Lean.Exception.getRef x = match x with | Lean.Exception.error ref x => ref | Lean.Exception.internal x x_1 => Lean.Syntax.missing

instance Lean.instInhabitedException :

Inhabited Lean.Exception

Equations

Lean.instInhabitedException = { default := Lean.Exception.error default default }

class Lean.AddErrorMessageContext (m : Type → Type) :

Type

add : Lean.Syntax → Lean.MessageData → m (Lean.Syntax × Lean.MessageData)

Instances

instance Lean.instAddErrorMessageContext (m : Type → Type) [inst : Lean.AddMessageContext m] [inst : Monad m] :

Lean.AddErrorMessageContext m

Equations

Lean.instAddErrorMessageContext m = { add := fun ref msg => do let msg ← Lean.addMessageContext msg pure (ref, msg) }

class Lean.MonadError (m : Type → Type) extends MonadExceptOf , Lean.MonadRef , Lean.AddErrorMessageContext :

Type 1

Instances

Lean.MonadError.mk

def Lean.throwError {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (msg : Lean.MessageData) :

m α

Equations

Lean.throwError msg = do let ref ← Lean.getRef let discr ← Lean.AddErrorMessageContext.add ref msg let x : Lean.Syntax × Lean.MessageData := discr match x with | (ref, msg) => throw (Lean.Exception.error ref msg)

def Lean.throwUnknownConstant {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m α

Equations

Lean.throwUnknownConstant constName = Lean.throwError (Lean.toMessageData "unknown constant '" ++ Lean.toMessageData (Lean.mkConst constName) ++ Lean.toMessageData "'")

def Lean.throwErrorAt {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (ref : Lean.Syntax) (msg : Lean.MessageData) :

m α

Equations

Lean.throwErrorAt ref msg = Lean.withRef ref (Lean.throwError msg)

def Lean.ofExcept {m : Type → Type} {ε : Type u_1} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : ToString ε] (x : Except ε α) :

m α

Equations

Lean.ofExcept x = match x with | Except.ok a => pure a | Except.error e => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format (toString e))

def Lean.throwKernelException {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (ex : Lean.KernelException) :

m α

Equations

Lean.throwKernelException ex = do let a ← Lean.getOptions Lean.throwError (Lean.KernelException.toMessageData ex a)

class Lean.MonadRecDepth (m : Type → Type) :

Type 1

withRecDepth : {α : Type} → Nat → m α → m α
getRecDepth : m Nat
getMaxRecDepth : m Nat

Instances

instance Lean.instMonadRecDepthReaderT {m : Type → Type} {ρ : Type} [inst : Monad m] [inst : Lean.MonadRecDepth m] :

Lean.MonadRecDepth (ReaderT ρ m)

Equations

Lean.instMonadRecDepthReaderT = { withRecDepth := fun {α} d x ctx => Lean.MonadRecDepth.withRecDepth d (x ctx), getRecDepth := fun x => Lean.MonadRecDepth.getRecDepth, getMaxRecDepth := fun x => Lean.MonadRecDepth.getMaxRecDepth }

instance Lean.instMonadRecDepthStateRefT' {m : Type → Type} {ω : Type} {σ : Type} [inst : Monad m] [inst : Lean.MonadRecDepth m] :

Lean.MonadRecDepth (StateRefT' ω σ m)

Equations

Lean.instMonadRecDepthStateRefT' = inferInstanceAs (Lean.MonadRecDepth (ReaderT (ST.Ref ω σ) fun α => m α))

instance Lean.instMonadRecDepthMonadCacheT {α : Type} {m : Type → Type} {ω : outParam Type} {β : Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : STWorld ω m] [inst : Lean.MonadRecDepth m] :

Lean.MonadRecDepth (Lean.MonadCacheT α β m)

Equations

Lean.instMonadRecDepthMonadCacheT = inferInstanceAs (Lean.MonadRecDepth (StateRefT' ω (Std.HashMap α β) m))

def Lean.throwMaxRecDepthAt {m : Type → Type} {α : Type} [inst : Lean.MonadError m] (ref : Lean.Syntax) :

m α

Equations

Lean.throwMaxRecDepthAt ref = throw (Lean.Exception.error ref (Lean.MessageData.ofFormat (Std.Format.text Lean.maxRecDepthErrorMessage)))

def Lean.Exception.isMaxRecDepth (ex : Lean.Exception) :

Equations

Lean.Exception.isMaxRecDepth ex = match ex with | Lean.Exception.error x (Lean.MessageData.ofFormat (Std.Format.text msg)) => msg == Lean.maxRecDepthErrorMessage | x => false

@[inline]

def Lean.withIncRecDepth {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : Lean.MonadRecDepth m] (x : m α) :

m α

Equations

Lean.withIncRecDepth x = do let curr ← Lean.MonadRecDepth.getRecDepth let max ← Lean.MonadRecDepth.getMaxRecDepth if (curr == max) = true then do let a ← Lean.getRef Lean.throwMaxRecDepthAt a else Lean.MonadRecDepth.withRecDepth (curr + 1) x

def Lean.termThrowError__ :

Lean.ParserDescr

Equations

Lean.termThrowError__ = Lean.ParserDescr.node `Lean.termThrowError__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "throwError ") (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.unary `interpolatedStr (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.cat `term 0)))

def Lean.termThrowErrorAt___ :

Lean.ParserDescr

Equations

Lean.termThrowErrorAt___ = Lean.ParserDescr.node `Lean.termThrowErrorAt___ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "throwErrorAt ") (Lean.ParserDescr.cat `term 1024)) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.unary `interpolatedStr (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.cat `term 0)))