- error: Lean.Syntax → Lean.MessageData → Lean.Exception
- internal: Lean.InternalExceptionId → optParam Lean.KVMap { entries := [] } → Lean.Exception
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Exception.getRef _fun_discr = match _fun_discr with | Lean.Exception.error ref msg => ref | Lean.Exception.internal id extra => 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 match discr 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
- One or more equations did not get rendered due to their size.
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}
{ω : 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 α
Return true if ex was generated by throwMaxRecDepthAt.
This function is a bit hackish. The max rec depth exception should probably be an internal exception,
but it is also produced by MacroM which implemented in the prelude, and internal exceptions have not
been defined yet.
Equations
- Lean.Exception.isMaxRecDepth ex = match ex with | Lean.Exception.error ref (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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.