opaque Lean.exportAttr : ParametricAttribute Name

@[export lean_get_export_name_for]

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

Equations

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

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

Equations

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