opaque Lean.neverExtractAttr : Lean.TagAttribute

@[export lean_has_never_extract_attribute]

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

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