opaque Lean.exportAttr : Lean.ParametricAttribute Lake.Name

@[export lean_get_export_name_for]

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

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