opaque Lean.Core.maxHeartbeats : Lean.Option Nat

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

Equations

• Lean.Core.getMaxHeartbeats opts = Lean.Option.get opts Lean.Core.maxHeartbeats * 1000

@[inline]

abbrev Lean.Core.InstantiateLevelCache : Type

Equations

• Lean.Core.InstantiateLevelCache = Lean.PersistentHashMap Lean.Name (List Lean.Level × Lean.Expr)

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

Equations

• Lean.Core.instInhabitedCache = { default := { instLevelType := default, instLevelValue := default } }

structure Lean.Core.State : Type

• Current environment.

  env : Lean.Environment

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

  nextMacroScope : Lean.MacroScope

• Name generator for producing unique FVarIds, MVarIds, and LMVarIds

  ngen : Lean.NameGenerator

• Trace messages

  traceState : Lean.TraceState

• Cache for instantiating universe polymorphic declarations.

  cache : Lean.Core.Cache

• Message log.

  messages : Lean.MessageLog

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

  infoState : Lean.Elab.InfoState

State for the CoreM monad.

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

Equations

• Lean.Core.instNonemptyState = Lean.Core.instNonemptyState.proof_1

structure Lean.Core.Context : Type

• Name of the file being compiled.

  fileName : String

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

  fileMap : Lean.FileMap
• options : Lean.Options
• currRecDepth : Nat
• maxRecDepth : Nat
• ref : Lean.Syntax
• currNamespace : Lean.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

Equations

• Lean.Core.instNonemptyContext = Lean.Core.instNonemptyContext.proof_1

@[inline]

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

Equations

• Lean.CoreM = ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception))

@[always_inline]

instance Lean.Core.instMonadCoreM : Monad Lean.CoreM

Equations

• Lean.Core.instMonadCoreM = let i := inferInstanceAs (Monad Lean.CoreM); Monad.mk

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

Equations

• Lean.Core.instInhabitedCoreM = { default := fun x x => throw default }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Core.instMonadOptionsCoreM = { getOptions := do let __do_lift ← read pure __do_lift.options }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Core.instAddMessageContextCoreM = { addMessageContext := Lean.addMessageContextPartial }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lean.Core.modifyInstLevelTypeCache f = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := f c₁, instLevelValue := c₂ }

@[inline]

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

Equations

• Lean.Core.modifyInstLevelValueCache f = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := c₁, instLevelValue := f c₂ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lean.Core.liftIOCore x = do let ref ← Lean.getRef liftM (IO.toEIO (fun err => Lean.Exception.error ref (Function.comp Lean.MessageData.ofFormat Std.format (toString err))) x)

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

Equations

• Lean.Core.instMonadLiftIOCoreM = { monadLift := fun {α} => Lean.Core.liftIOCore }

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

Equations

• One or more equations did not get rendered due to their size.

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

Restore backtrackable parts of the state.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.mkFreshUserName n = Lean.Core.mkFreshNameImp n

@[inline]

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

Equations

• Lean.Core.CoreM.run x ctx s = StateRefT'.run (x ctx) s

@[inline]

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

Equations

• Lean.Core.CoreM.run' x ctx s = Prod.fst <$> Lean.Core.CoreM.run x ctx s

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Core.withIncRecDepth x = controlAt Lean.CoreM fun runInBase => Lean.withIncRecDepth (runInBase x)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.checkMaxHeartbeats moduleName = do let __do_lift ← read Lean.Core.checkMaxHeartbeatsCore moduleName `maxHeartbeats __do_lift.maxHeartbeats

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

Equations

• Lean.withCurrHeartbeats x = controlAt Lean.CoreM fun runInBase => Lean.Core.withCurrHeartbeatsImp (runInBase x)

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Core.resetMessageLog : Lean.CoreM Unit

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Core.getMessageLog = do let __do_lift ← get pure __do_lift.messages

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.withAtLeastMaxRecDepth {m : Type → Type u_1} {α : Type} [inst : MonadFunctorT Lean.CoreM m] (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 : Monad m] [inst : MonadExcept Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) : 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 : Monad m] [inst : MonadExcept Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) : m α

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Creates the expression d → b

Equations

• Lean.mkArrow d b = do let __do_lift ← Lean.mkFreshUserName `x pure (Lean.mkForall __do_lift Lean.BinderInfo.default d b)

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

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_lcnf_compile_decls]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.addAndCompile decl = do Lean.addDecl decl Lean.compileDecl decl

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

Equations

• One or more equations did not get rendered due to their size.