@[reducible, inline]

abbrev Lean.Compiler.LCNF.DeclExtState : Type

Equations

• Lean.Compiler.LCNF.DeclExtState = Lean.PHashMap Lean.Name Lean.Compiler.LCNF.Decl

@[reducible, inline]

abbrev Lean.Compiler.LCNF.DeclExt : Type

Equations

• Lean.Compiler.LCNF.DeclExt = Lean.PersistentEnvExtension Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.DeclExtState

def Lean.Compiler.LCNF.mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt

Equations

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

opaque Lean.Compiler.LCNF.baseExt : PersistentEnvExtension Decl Decl DeclExtState

opaque Lean.Compiler.LCNF.monoExt : PersistentEnvExtension Decl Decl DeclExtState

def Lean.Compiler.LCNF.getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) : Option Decl

Equations

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

def Lean.Compiler.LCNF.getBaseDecl? (declName : Name) : CoreM (Option Decl)

Equations

• Lean.Compiler.LCNF.getBaseDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getDeclCore? __do_lift Lean.Compiler.LCNF.baseExt declName)

def Lean.Compiler.LCNF.getMonoDecl? (declName : Name) : CoreM (Option Decl)

Equations

• Lean.Compiler.LCNF.getMonoDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getDeclCore? __do_lift Lean.Compiler.LCNF.monoExt declName)

def Lean.Compiler.LCNF.saveBaseDeclCore (env : Environment) (decl : Decl) : Environment

Equations

• Lean.Compiler.LCNF.saveBaseDeclCore env decl = Lean.Compiler.LCNF.baseExt.addEntry (env.addExtraName decl.name) decl

def Lean.Compiler.LCNF.saveMonoDeclCore (env : Environment) (decl : Decl) : Environment

Equations

• Lean.Compiler.LCNF.saveMonoDeclCore env decl = Lean.Compiler.LCNF.monoExt.addEntry (env.addExtraName decl.name) decl

def Lean.Compiler.LCNF.Decl.saveBase (decl : Decl) : CoreM Unit

Equations

• decl.saveBase = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveBaseDeclCore x decl

def Lean.Compiler.LCNF.Decl.saveMono (decl : Decl) : CoreM Unit

Equations

• decl.saveMono = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveMonoDeclCore x decl

def Lean.Compiler.LCNF.Decl.save (decl : Decl) : CompilerM Unit

Equations

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

def Lean.Compiler.LCNF.getDeclAt? (declName : Name) (phase : Phase) : CoreM (Option Decl)

Equations

• Lean.Compiler.LCNF.getDeclAt? declName Lean.Compiler.LCNF.Phase.base = Lean.Compiler.LCNF.getBaseDecl? declName
• Lean.Compiler.LCNF.getDeclAt? declName Lean.Compiler.LCNF.Phase.mono = Lean.Compiler.LCNF.getMonoDecl? declName
• Lean.Compiler.LCNF.getDeclAt? declName phase = pure none

def Lean.Compiler.LCNF.getDecl? (declName : Name) : CompilerM (Option Decl)

Equations

• Lean.Compiler.LCNF.getDecl? declName = do let __do_lift ← Lean.Compiler.LCNF.getPhase liftM (Lean.Compiler.LCNF.getDeclAt? declName __do_lift)

def Lean.Compiler.LCNF.getExt (phase : Phase) : DeclExt

Equations

• Lean.Compiler.LCNF.getExt Lean.Compiler.LCNF.Phase.base = Lean.Compiler.LCNF.baseExt
• Lean.Compiler.LCNF.getExt Lean.Compiler.LCNF.Phase.mono = Lean.Compiler.LCNF.monoExt
• Lean.Compiler.LCNF.getExt phase = panicWithPosWithDecl "Lean.Compiler.LCNF.PhaseExt" "Lean.Compiler.LCNF.getExt" 82 9 "unreachable code has been reached"

def Lean.Compiler.LCNF.forEachDecl (f : Decl → CoreM Unit) (phase : Phase := Phase.base) : CoreM Unit

Equations

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

def Lean.Compiler.LCNF.forEachModuleDecl (moduleName : Name) (f : Decl → CoreM Unit) (phase : Phase := Phase.base) : CoreM Unit

Equations

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

def Lean.Compiler.LCNF.forEachMainModuleDecl (f : Decl → CoreM Unit) (phase : Phase := Phase.base) : CoreM Unit

Equations

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