Documentation

Lean.Compiler.NeverExtractAttr

source
opaque Lean.neverExtractAttr:
Lean.TagAttribute
source
@[export lean_has_never_extract_attribute]
def Lean.hasNeverExtractAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
partial def Lean.hasNeverExtractAttribute.visit (env : Lean.Environment) (n : Lean.Name) :
Bool