Lean.Compiler.LCNF.PhaseExt

source

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

Bool

Instances For

source

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

Environment

Instances For

source

@[reducible, inline]

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

Type

Instances For

source

@[reducible, inline]

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

Type

Instances For

source

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

Type

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedDeclExt {pu : Purity} :

Inhabited (DeclExt pu)

source

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

IO (DeclExt phase.toPurity)

Instances For

source

opaque Lean.Compiler.LCNF.baseExt :

DeclExt Purity.pure

source

opaque Lean.Compiler.LCNF.monoExt :

DeclExt Purity.pure

source

opaque Lean.Compiler.LCNF.impureExt :

EnvExtension (DeclExtState Purity.impure)

source

@[reducible, inline]

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

Type

Instances For

source

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

Type

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedSigExt {pu : Purity} :

Inhabited (SigExt pu)

source

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

IO (SigExt phase.toPurity)

Instances For

source

opaque Lean.Compiler.LCNF.impureSigExt :

SigExt Purity.impure

source

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

Option (Decl pu)

Instances For

source

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

Option (Signature pu)

Instances For

source

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

CoreM (Option (Decl Purity.pure))

Instances For

source

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

CoreM (Option (Decl Purity.pure))

Instances For

source

def Lean.Compiler.LCNF.getLocalImpureDecl? (declName : Name) :

CoreM (Option (Decl Purity.impure))

Instances For

source

def Lean.Compiler.LCNF.getImpureSignature? (declName : Name) :

CoreM (Option (Signature Purity.impure))

Instances For

source

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

Environment

Instances For

source

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

Environment

Instances For

source

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

Environment

Instances For

source

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

CoreM Unit

Instances For

source

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

CoreM Unit

Instances For

source

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

CoreM Unit

Instances For

source

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

CompilerM Unit

Instances For

source

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

CoreM (Option (Decl phase.toPurity))

Instances For

source

@[inline]

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

CompilerM (Option ((pu : Purity) × Decl pu))

Instances For

source

def Lean.Compiler.LCNF.getLocalDeclAt? (declName : Name) (phase : Phase) :

CompilerM (Option (Decl phase.toPurity))

Instances For

source

@[inline]

def Lean.Compiler.LCNF.getLocalDecl? (declName : Name) :

CompilerM (Option ((pu : Purity) × Decl pu))

Instances For