def Lean.markMeta (env : Environment) (declName : Name) : Environment

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

Equations

• Lean.markMeta env declName = Lean.metaExt✝.tag env declName

def Lean.markNotMeta (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

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

def Lean.isMarkedMeta (env : Environment) (declName : Name) : Bool

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

Equations

• Lean.isMarkedMeta env declName = Lean.metaExt✝.isTagged env declName

def Lean.isDeclMeta (env : Environment) (declName : Name) : Bool

Whether a declaration should be exported for interpretation.

Equations

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

def Lean.setDeclMeta (env : Environment) (declName : Name) : Environment

Marks a declaration to be exported for interpretation.

Equations

• Lean.setDeclMeta env declName = if Lean.isDeclMeta env declName = true then env else Lean.PersistentEnvExtension.addEntry Lean.declMetaExt✝ env declName

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.