Documentation
Lean
.
Compiler
.
ExportAttr
Search
return to top
source
Imports
Lean.Attributes
Imported by
Lean
.
exportAttr
Lean
.
getExportNameFor?
Lean
.
isExport
source
opaque
Lean
.
exportAttr
:
ParametricAttribute
Name
source
@[export lean_get_export_name_for]
def
Lean
.
getExportNameFor?
(
env
:
Environment
)
(
n
:
Name
)
:
Option
Name
Equations
Instances For
source
def
Lean
.
isExport
(
env
:
Environment
)
(
n
:
Name
)
:
Bool
Equations
Instances For