opaque Lean.metaExt : TagDeclarationExtension

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

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

@[export lean_get_ir_phases]

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.