opaque Lean.exportAttr : Lean.ParametricAttribute Lean.Name

@[export lean_get_export_name_for]

def Lean.getExportNameFor? (env : Lean.Environment) (n : Lean.Name) : Option Lean.Name

Equations

• Lean.getExportNameFor? env n = Lean.ParametricAttribute.getParam? Lean.exportAttr env n

def Lean.isExport (env : Lean.Environment) (n : Lean.Name) : Bool

Equations

• Lean.isExport env n = (Option.isSome (Lean.getExportNameFor? env n) || n == `main)