inductive Lean.IR.LogEntry : Type

• step (cls : Name) (decls : Array Decl) : LogEntry
• message (msg : Format) : LogEntry

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

@[implicit_reducible]

instance Lean.IR.LogEntry.instToFormat : ToFormat LogEntry

@[reducible, inline]

abbrev Lean.IR.Log : Type

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

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

@[reducible, inline]

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

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

def Lean.IR.tracePrefixOptionName : Name

@[inline]

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

@[inline]

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

@[inline]

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

@[reducible, inline]

abbrev Lean.IR.DeclMap : Type

opaque Lean.IR.declMapExt : SimplePersistentEnvExtension Decl DeclMap

def Lean.IR.findEnvDecl (env : Environment) (declName : Name) (includeServer : Bool := false) : Option Decl

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

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

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

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

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

Returns the list of IR declarations in reverse declaration order.

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

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

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

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

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

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

@[export lean_decl_get_sorry_dep]

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