Documentation

Lean.Compiler.ExportAttr

constant Lean.exportAttr :

Lean.ParametricAttribute Lean.Name

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) :

Equations

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