Lean4
@[inherit_doc linter.style.nameCheck]
def doubleUnderscore : Linter where
run :=
withSetOptionIn fun stx => do
unless getLinterValue linter.style.nameCheck (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
let mut aliases := #[]
if let some exp := stx.find? (·.isOfKind `Lean.Parser.Command.export) then
aliases ← getAliasSyntax exp
for id in aliases.push ((stx.find? (·.isOfKind ``declId)).getD default)[0]do
let declName := id.getId
if id.getPos? == some default then
continue
if declName.hasMacroScopes then
continue
if id.getKind == `ident then
-- Check whether the declaration name contains "__".
if 1 < (declName.toString.splitOn "__").length then
Linter.logLint linter.style.nameCheck id
m! "The declaration '{id}' contains '__', which does not follow the mathlib naming \
conventions. Consider using single underscores instead."
