def Lean.Compiler.LCNF.isDeclTransparent (env : Environment) (phase : Phase) (declName : Name) : Bool

def Lean.Compiler.LCNF.setDeclTransparent (env : Environment) (phase : Phase) (declName : Name) : Environment

@[reducible, inline]

abbrev Lean.Compiler.LCNF.AbstractDeclExtState (pu : Purity) (β : Purity → Type) : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.DeclExtState (pu : Purity) : Type

def Lean.Compiler.LCNF.DeclExt (pu : Purity) : Type

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedDeclExt {pu : Purity} : Inhabited (DeclExt pu)

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

opaque Lean.Compiler.LCNF.baseExt : DeclExt Purity.pure

opaque Lean.Compiler.LCNF.monoExt : DeclExt Purity.pure

opaque Lean.Compiler.LCNF.impureExt : EnvExtension (DeclExtState Purity.impure)

@[reducible, inline]

abbrev Lean.Compiler.LCNF.SigExtState (pu : Purity) : Type

def Lean.Compiler.LCNF.SigExt (pu : Purity) : Type

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedSigExt {pu : Purity} : Inhabited (SigExt pu)

def Lean.Compiler.LCNF.mkSigDeclExt (phase : Phase) (name : Name := by exact decl_name%) : IO (SigExt phase.toPurity)

opaque Lean.Compiler.LCNF.impureSigExt : SigExt Purity.impure

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

def Lean.Compiler.LCNF.getSigCore? {pu : Purity} (env : Environment) (ext : SigExt pu) (declName : Name) : Option (Signature pu)

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

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

def Lean.Compiler.LCNF.getLocalImpureDecl? (declName : Name) : CoreM (Option (Decl Purity.impure))

def Lean.Compiler.LCNF.getLocalImpureDecls : CoreM (Array Name)

def Lean.Compiler.LCNF.getImpureSignature? (declName : Name) : CoreM (Option (Signature Purity.impure))

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

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

def Lean.Compiler.LCNF.saveImpureDeclCore (env : Environment) (decl : Decl Purity.impure) : Environment

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

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

def Lean.Compiler.LCNF.Decl.saveImpure (decl : Decl Purity.impure) : CoreM Unit

def Lean.Compiler.LCNF.Decl.save {pu : Purity} (decl : Decl pu) : CompilerM Unit

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

@[inline]

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

def Lean.Compiler.LCNF.getLocalDeclAt? (declName : Name) (phase : Phase) : CompilerM (Option (Decl phase.toPurity))

@[inline]

def Lean.Compiler.LCNF.getLocalDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl pu))

opaque Lean.Compiler.LCNF.declOrderExt : EnvExtension (List Name × NameSet)

def Lean.Compiler.LCNF.recordFinalImpureDecl (env : Environment) (name : Name) : Environment

def Lean.Compiler.LCNF.getImpureDeclIndices (env : Environment) (targets : Array Name) : Std.HashMap Name Nat