inductive Lean.IR.LogEntry : Type

• step: Lake.Name → Array Lean.IR.Decl → Lean.IR.LogEntry
• message: Lean.Format → Lean.IR.LogEntry

def Lean.IR.LogEntry.fmt : Lean.IR.LogEntry → Lean.Format

instance Lean.IR.LogEntry.instToFormatLogEntry : Lean.ToFormat Lean.IR.LogEntry

@[inline, reducible]

abbrev Lean.IR.Log : Type

def Lean.IR.Log.format (log : Lean.IR.Log) : Lean.Format

@[export lean_ir_log_to_string]

def Lean.IR.Log.toString (log : Lean.IR.Log) : String

structure Lean.IR.CompilerState : Type

• env : Lean.Environment
• log : Lean.IR.Log

@[inline, reducible]

abbrev Lean.IR.CompilerM (α : Type) : Type

def Lean.IR.log (entry : Lean.IR.LogEntry) : Lean.IR.CompilerM Unit

def Lean.IR.tracePrefixOptionName : Lake.Name

@[inline]

def Lean.IR.logDecls (cls : Lake.Name) (decl : Array Lean.IR.Decl) : Lean.IR.CompilerM Unit

@[inline]

def Lean.IR.logMessageIf {α : Type} [Lean.ToFormat α] (cls : Lake.Name) (a : α) : Lean.IR.CompilerM Unit

@[inline]

def Lean.IR.logMessage {α : Type} [Lean.ToFormat α] (a : α) : Lean.IR.CompilerM Unit

@[inline]

def Lean.IR.modifyEnv (f : Lean.Environment → Lean.Environment) : Lean.IR.CompilerM Unit

@[inline, reducible]

abbrev Lean.IR.DeclMap : Type

opaque Lean.IR.declMapExt : Lean.SimplePersistentEnvExtension Lean.IR.Decl Lean.IR.DeclMap

@[export lean_ir_find_env_decl]

def Lean.IR.findEnvDecl (env : Lean.Environment) (declName : Lake.Name) : Option Lean.IR.Decl

def Lean.IR.findDecl (n : Lake.Name) : Lean.IR.CompilerM (Option Lean.IR.Decl)

def Lean.IR.containsDecl (n : Lake.Name) : Lean.IR.CompilerM Bool

def Lean.IR.getDecl (n : Lake.Name) : Lean.IR.CompilerM Lean.IR.Decl

@[export lean_ir_add_decl]

def Lean.IR.addDeclAux (env : Lean.Environment) (decl : Lean.IR.Decl) : Lean.Environment

def Lean.IR.getDecls (env : Lean.Environment) : List Lean.IR.Decl

def Lean.IR.getEnv : Lean.IR.CompilerM Lean.Environment

def Lean.IR.addDecl (decl : Lean.IR.Decl) : Lean.IR.CompilerM Unit

def Lean.IR.addDecls (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM Unit

def Lean.IR.findEnvDecl' (env : Lean.Environment) (n : Lake.Name) (decls : Array Lean.IR.Decl) : Option Lean.IR.Decl

def Lean.IR.findDecl' (n : Lake.Name) (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM (Option Lean.IR.Decl)

def Lean.IR.containsDecl' (n : Lake.Name) (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM Bool

def Lean.IR.getDecl' (n : Lake.Name) (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM Lean.IR.Decl

@[export lean_decl_get_sorry_dep]

def Lean.IR.getSorryDep (env : Lean.Environment) (declName : Lake.Name) : Option Lake.Name