Documentation

Lean.Compiler.NeverExtractAttr

source
constant Lean.neverExtractAttr :
Lean.TagAttribute
source
def Lean.hasNeverExtractAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
partial def Lean.hasNeverExtractAttribute.visit (env : Lean.Environment) (n : Lean.Name) :
Bool