source
def Lean.addMeta (env : Environment) (declName : Name) :
Environment

Marks in the environment extension that the given declaration has been declared by the user as `meta`.

Equations

- Lean.addMeta env declName = Lean.metaExt✝.tag env declName

Instances For

source
def Lean.addNotMeta (env : Environment) (declName : Name) :
Environment

Marks the given declaration as not being annotated with `meta` even if it could have been by the user.

Equations

- Lean.addNotMeta env declName = if declName.isAnonymous = true then env else Lean.notMetaExt✝.modifyState env (fun (x : Lean.NameSet) => x.insert declName) Lean.notMetaExt✝¹.asyncMode declName

Instances For

source
def Lean.isMeta (env : Environment) (declName : Name) :
Bool

Returns true iff the user has declared the given declaration as `meta`.

Equations

- Lean.isMeta env declName = Lean.metaExt✝.isTagged env declName

Instances For

source
def Lean.getIRPhases (env : Environment) (declName : Name) :
IRPhases

Returns the IR phases of the given declaration that should be considered accessible. Does not take additional IR loaded for language server purposes into account.

Equations

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

Instances For