@[inline]

abbrev Lean.Compiler.LCNF.BaseExtState : Type

Equations

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

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

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

Equations

• Lean.Compiler.LCNF.getBaseDecl? declName = do let a ← Lean.getEnv pure (Lean.Compiler.LCNF.getBaseDeclCore? a declName)

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

Equations

• Lean.Compiler.LCNF.saveBaseDeclCore env decl = let env := Lean.Environment.addExtraName env decl.name; Lean.PersistentEnvExtension.addEntry Lean.Compiler.LCNF.baseExt env decl

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

Equations

• Lean.Compiler.LCNF.Decl.saveBase decl = Lean.modifyEnv fun a => Lean.Compiler.LCNF.saveBaseDeclCore a decl

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

Equations

• Lean.Compiler.LCNF.getDeclAt? declName phase = match phase with | Lean.Compiler.LCNF.Phase.base => Lean.Compiler.LCNF.getBaseDecl? declName | x => pure none

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

Equations

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

def Lean.Compiler.LCNF.normalizeFVarIds (decl : Lean.Compiler.LCNF.Decl) : Lean.CoreM Lean.Compiler.LCNF.Decl

Equations

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

def Lean.Compiler.LCNF.saveBase : Lean.Compiler.LCNF.Pass

Equations

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

def Lean.Compiler.LCNF.forEachDecl (f : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) : Lean.CoreM Unit

Equations

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

def Lean.Compiler.LCNF.forEachModuleDecl (moduleName : Lean.Name) (f : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) : 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) : Lean.CoreM Unit

Equations

• Lean.Compiler.LCNF.forEachMainModuleDecl f = do let a ← Lean.getEnv Lean.PersistentHashMap.forM (Lean.PersistentEnvExtension.getState Lean.Compiler.LCNF.baseExt a) fun x decl => f decl