opaque Lean.neverExtractAttr : Lean.TagAttribute

@[export lean_has_never_extract_attribute]

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

Equations

• Lean.hasNeverExtractAttribute env n = Lean.hasNeverExtractAttribute.visit env n

partial def Lean.hasNeverExtractAttribute.visit (env : Lean.Environment) (n : Lake.Name) : Bool