Documentation

Lean.Exception

inductive Lean.Exception :
Type
Equations
instance Lean.instAddErrorMessageContext (m : TypeType) [inst : Lean.AddMessageContext m] [inst : Monad m] :
Equations
class Lean.MonadError (m : TypeType) extends MonadExceptOf , Lean.MonadRef , Lean.AddErrorMessageContext :
Type 1
Instances
def Lean.throwError {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (msg : Lean.MessageData) :
m α
Equations
def Lean.throwUnknownConstant {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (constName : Lean.Name) :
m α
Equations
def Lean.throwErrorAt {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] (ref : Lean.Syntax) (msg : Lean.MessageData) :
m α
Equations
def Lean.ofExcept {m : TypeType} {ε : Type u_1} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : ToString ε] (x : Except ε α) :
m α
Equations
def Lean.throwKernelException {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (ex : Lean.KernelException) :
m α
Equations
class Lean.MonadRecDepth (m : TypeType) :
Type 1
  • withRecDepth : {α : Type} → Natm αm α
  • getRecDepth : m Nat
  • getMaxRecDepth : m Nat
Instances
instance Lean.instMonadRecDepthReaderT {m : TypeType} {ρ : Type} [inst : Monad m] [inst : Lean.MonadRecDepth 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 : TypeType} {ω : Type} {σ : Type} [inst : Monad m] [inst : Lean.MonadRecDepth m] :
Equations
instance Lean.instMonadRecDepthMonadCacheT {α : Type} {m : TypeType} {ω : outParam Type} {β : Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : STWorld ω m] [inst : Lean.MonadRecDepth m] :
Equations
@[inline]
def Lean.withIncRecDepth {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadError m] [inst : Lean.MonadRecDepth m] (x : m α) :
m α
Equations