opaque Lean.Core.maxHeartbeats : Lean.Option Nat

def Lean.Core.getMaxHeartbeats (opts : Lean.Options) : Nat

@[inline, reducible]

abbrev Lean.Core.InstantiateLevelCache : Type

structure Lean.Core.Cache : Type

• instLevelType : Lean.Core.InstantiateLevelCache
• instLevelValue : Lean.Core.InstantiateLevelCache

Cache for the CoreM monad

instance Lean.Core.instInhabitedCache : Inhabited Lean.Core.Cache

structure Lean.Core.State : Type

• env : Lean.Environment

  Current environment.

• nextMacroScope : Lean.MacroScope

  Next macro scope. We use macro scopes to avoid accidental name capture.

• ngen : Lean.NameGenerator

  Name generator for producing unique FVarIds, MVarIds, and LMVarIds

• traceState : Lean.TraceState

  Trace messages

• cache : Lean.Core.Cache

  Cache for instantiating universe polymorphic declarations.

• messages : Lean.MessageLog

  Message log.

• infoState : Lean.Elab.InfoState

  Info tree. We have the info tree here because we want to update it while adding attributes.

State for the CoreM monad.

instance Lean.Core.instNonemptyState : Nonempty Lean.Core.State

structure Lean.Core.Context : Type

• fileName : String

  Name of the file being compiled.

• fileMap : Lean.FileMap

  Auxiliary datastructure for converting String.Pos into Line/Column number.

• options : Lean.Options
• currRecDepth : Nat
• maxRecDepth : Nat
• ref : Lean.Syntax
• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl
• initHeartbeats : Nat
• maxHeartbeats : Nat
• currMacroScope : Lean.MacroScope

Context for the CoreM monad.

instance Lean.Core.instNonemptyContext : Nonempty Lean.Core.Context

@[inline, reducible]

abbrev Lean.Core.CoreM (α : Type) : 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

@[always_inline]

instance Lean.Core.instMonadCoreM : Monad Lean.CoreM

instance Lean.Core.instInhabitedCoreM {α : Type} : Inhabited (Lean.CoreM α)

instance Lean.Core.instMonadRefCoreM : Lean.MonadRef Lean.CoreM

instance Lean.Core.instMonadEnvCoreM : Lean.MonadEnv Lean.CoreM

instance Lean.Core.instMonadOptionsCoreM : Lean.MonadOptions Lean.CoreM

instance Lean.Core.instMonadWithOptionsCoreM : Lean.MonadWithOptions Lean.CoreM

instance Lean.Core.instAddMessageContextCoreM : Lean.AddMessageContext Lean.CoreM

instance Lean.Core.instMonadNameGeneratorCoreM : Lean.MonadNameGenerator Lean.CoreM

instance Lean.Core.instMonadRecDepthCoreM : Lean.MonadRecDepth Lean.CoreM

instance Lean.Core.instMonadResolveNameCoreM : Lean.MonadResolveName Lean.CoreM

def Lean.Core.withFreshMacroScope {α : Type} (x : Lean.CoreM α) : Lean.CoreM α

instance Lean.Core.instMonadQuotationCoreM : Lean.MonadQuotation Lean.CoreM

instance Lean.Core.instMonadInfoTreeCoreM : Lean.Elab.MonadInfoTree Lean.CoreM

@[inline]

def Lean.Core.modifyCache (f : Lean.Core.Cache → Lean.Core.Cache) : Lean.CoreM Unit

@[inline]

def Lean.Core.modifyInstLevelTypeCache (f : Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) : Lean.CoreM Unit

@[inline]

def Lean.Core.modifyInstLevelValueCache (f : Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) : Lean.CoreM Unit

def Lean.Core.instantiateTypeLevelParams (c : Lean.ConstantInfo) (us : List Lean.Level) : Lean.CoreM Lean.Expr

def Lean.Core.instantiateValueLevelParams (c : Lean.ConstantInfo) (us : List Lean.Level) : Lean.CoreM Lean.Expr

@[inline]

def Lean.Core.liftIOCore {α : Type} (x : IO α) : Lean.CoreM α

instance Lean.Core.instMonadLiftIOCoreM : MonadLift IO Lean.CoreM

instance Lean.Core.instMonadTraceCoreM : Lean.MonadTrace Lean.CoreM

def Lean.Core.restore (b : Lean.Core.State) : Lean.CoreM Unit

Restore backtrackable parts of the state.

def Lean.Core.mkFreshUserName (n : Lake.Name) : Lean.CoreM Lake.Name

@[inline]

def Lean.Core.CoreM.run {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) : EIO Lean.Exception (α × Lean.Core.State)

@[inline]

def Lean.Core.CoreM.run' {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) : EIO Lean.Exception α

@[inline]

def Lean.Core.CoreM.toIO {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) : IO (α × Lean.Core.State)

instance Lean.Core.instMetaEvalCoreM {α : Type} [Lean.MetaEval α] : Lean.MetaEval (Lean.CoreM α)

def Lean.Core.withIncRecDepth {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT Lean.CoreM m] (x : m α) : m α

def Lean.Core.throwMaxHeartbeat (moduleName : Lake.Name) (optionName : Lake.Name) (max : Nat) : Lean.CoreM Unit

def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Lake.Name) (max : Nat) : Lean.CoreM Unit

def Lean.Core.checkMaxHeartbeats (moduleName : String) : Lean.CoreM Unit

def Lean.Core.withCurrHeartbeats {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT Lean.CoreM m] (x : m α) : m α

def Lean.Core.setMessageLog (messages : Lean.MessageLog) : Lean.CoreM Unit

def Lean.Core.resetMessageLog : Lean.CoreM Unit

def Lean.Core.getMessageLog : Lean.CoreM Lean.MessageLog

instance Lean.Core.instMonadLogCoreM : Lean.MonadLog Lean.CoreM

@[inline]

def Lean.withAtLeastMaxRecDepth {m : Type → Type u_1} {α : Type} [MonadFunctorT Lean.CoreM m] (max : Nat) : m α → m α

@[inline]

def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) : m α

@[inline]

def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) : m α

def Lean.Exception.isMaxHeartbeat (ex : Lean.Exception) : Bool

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

def Lean.mkArrow (d : Lean.Expr) (b : Lean.Expr) : Lean.CoreM Lean.Expr

Creates the expression d → b

def Lean.addDecl (decl : Lean.Declaration) : Lean.CoreM Unit

opaque Lean.compiler.enableNew : Lean.Option Bool

@[extern lean_lcnf_compile_decls]

opaque Lean.compileDeclsNew (declNames : List Lake.Name) : Lean.CoreM Unit

def Lean.compileDecl (decl : Lean.Declaration) : Lean.CoreM Unit

def Lean.compileDecls (decls : List Lake.Name) : Lean.CoreM Unit

def Lean.addAndCompile (decl : Lean.Declaration) : Lean.CoreM Unit

def Lean.ImportM.runCoreM {α : Type} (x : Lean.CoreM α) : Lean.ImportM α