- error: Lean.Syntax → Lean.MessageData → Lean.Exception
- internal: Lean.InternalExceptionId → optParam Lean.KVMap { entries := [] } → Lean.Exception
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)
Equations
- Lean.Exception.getRef x = match x with | Lean.Exception.error ref x => ref | Lean.Exception.internal x x_1 => Lean.Syntax.missing
Equations
- Lean.instInhabitedException = { default := Lean.Exception.error default default }
- add : Lean.Syntax → Lean.MessageData → m (Lean.Syntax × Lean.MessageData)
instance
Lean.instAddErrorMessageContext
(m : Type → Type)
[inst : Lean.AddMessageContext m]
[inst : Monad 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
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)
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
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
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)))
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)))