inductive Lean.IR.LogEntry : Type

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

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

instance Lean.IR.LogEntry.instToFormat : ToFormat LogEntry

@[reducible, inline]

abbrev Lean.IR.Log : Type

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

@[export lean_ir_log_to_string]

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

structure Lean.IR.CompilerState : Type

• env : Environment
• log : Log

@[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

@[inline]

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

@[reducible, inline]

abbrev Lean.IR.DeclMap : Type

@[reducible, inline]

abbrev Lean.IR.CollectUsedFDecls.M (α : Type) : Type

@[inline]

def Lean.IR.CollectUsedFDecls.collect (f : FunId) : M Unit

partial def Lean.IR.CollectUsedFDecls.collectFnBody : FnBody → M Unit

def Lean.IR.CollectUsedFDecls.collectDecl : Decl → M NameSet

def Lean.IR.collectUsedFDecls (decl : Decl) (used : NameSet := ∅) : NameSet

Adds to used all Decl.fdecls referenced directly by decl.

def Lean.IR.getFDeclClosure (m : DeclMap) (decls : Array Decl) : NameSet

Computes the closure of Decl.fdecls referenced by decl.

opaque Lean.IR.declMapExt : SimplePersistentEnvExtension Decl DeclMap

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

Retrieves IR for codegen purposes, i.e. independent of meta import.

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

@[export lean_ir_add_decl]

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

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

def Lean.IR.getEnv : CompilerM Environment

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