# Documentation

Lean.CoreM

@[inline]
Equations

Cache for the CoreM monad

Instances For
Equations

Instances For

Instances For
@[inline]
abbrev Lean.Core.CoreM (α : Type) :

CoreM is a monad for manipulating the Lean environment. It is the base monad for MetaM. The main features it provides are:

• name generator state
• environment state
• Lean options context
• the current open namespace
Equations
@[always_inline]
Equations
Equations
• Lean.Core.instInhabitedCoreM = { default := fun x x => throw default }
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
Equations
• One or more equations did not get rendered due to their size.
Equations
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.
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.
@[inline]
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := f c₁, instLevelValue := c₂ }
@[inline]
Equations
• = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := c₁, instLevelValue := f c₂ }
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.
@[inline]
def Lean.Core.liftIOCore {α : Type} (x : IO α) :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.

Restore backtrackable parts of the state.

Equations
• One or more equations did not get rendered due to their size.
Equations
@[inline]
def Lean.Core.CoreM.run {α : Type} (x : ) (ctx : Lean.Core.Context) (s : Lean.Core.State) :
Equations
@[inline]
Equations
@[inline]
def Lean.Core.CoreM.toIO {α : Type} (x : ) (ctx : Lean.Core.Context) (s : Lean.Core.State) :
IO ()
Equations
• One or more equations did not get rendered due to their size.
instance Lean.Core.instMetaEvalCoreM {α : Type} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Core.withIncRecDepth {m : TypeType u_1} {α : Type} [inst : ] [inst : ] (x : m α) :
m α
Equations
def Lean.Core.throwMaxHeartbeat (moduleName : Lean.Name) (optionName : Lean.Name) (max : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Lean.Name) (max : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.Core.withCurrHeartbeats {m : TypeType u_1} {α : Type} [inst : ] [inst : ] (x : m α) :
m α
Equations
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
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.withAtLeastMaxRecDepth {m : TypeType u_1} {α : Type} [inst : ] (max : Nat) :
m αm α
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [inst : ] [inst : ] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.Exceptionm α) :
m α
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [inst : ] [inst : ] (ids : ) (x : m α) (h : Lean.Exceptionm α) :
m α
Equations
• One or more equations did not get rendered due to their size.

Return true if ex was generated by throwMaxHeartbeat. This function is a bit hackish. The heartbeat exception should probably be an internal exception. We used a similar hack at Exception.isMaxRecDepth

Equations
• One or more equations did not get rendered due to their size.
def Lean.mkArrow (d : Lean.Expr) (b : Lean.Expr) :

Creates the expression d → b

Equations
Equations
• One or more equations did not get rendered due to their size.
@[extern lean_lcnf_compile_decls]
opaque Lean.compileDeclsNew (declNames : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.compileDecls (decls : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.ImportM.runCoreM {α : Type} (x : ) :
Equations
• One or more equations did not get rendered due to their size.