@[reducible, inline]

abbrev Lean.Compiler.LCNF.DeclExtState : Type

Equations

• Lean.Compiler.LCNF.DeclExtState = Lean.PHashMap Lake.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 : autoParam Lake.Name _auto✝) : IO Lean.Compiler.LCNF.DeclExt

Equations

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

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

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

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

Equations

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

def Lean.Compiler.LCNF.getBaseDecl? (declName : Lake.Name) : Lean.CoreM (Option Lean.Compiler.LCNF.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 : Lake.Name) : Lean.CoreM (Option Lean.Compiler.LCNF.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 : Lean.Environment) (decl : Lean.Compiler.LCNF.Decl) : Lean.Environment

Equations

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

def Lean.Compiler.LCNF.saveMonoDeclCore (env : Lean.Environment) (decl : Lean.Compiler.LCNF.Decl) : Lean.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 : Lean.Compiler.LCNF.Decl) : Lean.CoreM Unit

Equations

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.getDeclAt? (declName : Lake.Name) (phase : Lean.Compiler.LCNF.Phase) : Lean.CoreM (Option Lean.Compiler.LCNF.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 : Lake.Name) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.Phase) : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) : Lean.CoreM Unit

Equations

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

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

Equations

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

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

Equations

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