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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.AbstractDeclExtState pu β = Lean.PHashMap Lean.Name (β pu)

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.DeclExtState pu = Lean.Compiler.LCNF.AbstractDeclExtState pu Lean.Compiler.LCNF.Decl

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

Equations

• Lean.Compiler.LCNF.DeclExt pu = Lean.PersistentEnvExtension (Lean.Compiler.LCNF.Decl pu) (Lean.Compiler.LCNF.Decl pu) (Lean.Compiler.LCNF.DeclExtState pu)

@[instance_reducible]

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.SigExtState pu = Lean.Compiler.LCNF.AbstractDeclExtState pu Lean.Compiler.LCNF.Signature

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

Equations

• Lean.Compiler.LCNF.SigExt pu = Lean.PersistentEnvExtension (Lean.Compiler.LCNF.Signature pu) (Lean.Compiler.LCNF.Signature pu) (Lean.Compiler.LCNF.SigExtState pu)

@[instance_reducible]

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

Equations

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

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

Equations

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

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)

Equations

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

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

Equations

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

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

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 Purity.pure))

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.getLocalImpureDecl? (declName : Name) : CoreM (Option (Decl Purity.impure))

Equations

• Lean.Compiler.LCNF.getLocalImpureDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.Compiler.LCNF.impureExt.getState __do_lift) declName)

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

Equations

• Lean.Compiler.LCNF.getImpureSignature? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getSigCore? __do_lift Lean.Compiler.LCNF.impureSigExt declName)

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

Equations

• Lean.Compiler.LCNF.saveBaseDeclCore env decl = Lean.PersistentEnvExtension.addEntry Lean.Compiler.LCNF.baseExt env decl

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

Equations

• Lean.Compiler.LCNF.saveMonoDeclCore env decl = Lean.PersistentEnvExtension.addEntry Lean.Compiler.LCNF.monoExt env decl

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

Equations

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

def Lean.Compiler.LCNF.Decl.saveBase (decl : Decl Purity.pure) : 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 Purity.pure) : CoreM Unit

Equations

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

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

Equations

• decl.saveImpure = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveImpureDeclCore x decl

def Lean.Compiler.LCNF.Decl.save {pu : Purity} (decl : Decl pu) : 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 phase.toPurity))

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 Lean.Compiler.LCNF.Phase.impure = Lean.throwError (Lean.toMessageData "Internal compiler error: getDecl? on impure is unuspported for now")

@[inline]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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