2b8c273687
This PR adds a `linter.redundantVisibility` option (default `true`) that warns when a visibility modifier has no effect because it matches the default for the current context: - `private` outside a `public section` in a `module` file, where declarations are already module-scoped by default - `public` in a non-`module` file or inside a `public section`, where declarations are already public by default The check is integrated directly into `elabModifiers` so it covers all declaration types uniformly. --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
53 lines
1.4 KiB
Text
53 lines
1.4 KiB
Text
module
|
|
|
|
set_option linter.redundantVisibility true
|
|
|
|
-- `private` outside `public section` should warn
|
|
/--
|
|
warning: `private` has no effect in a `module` file outside `public section`; declarations are already `private` by default
|
|
|
|
Note: This linter can be disabled with `set_option linter.redundantVisibility false`
|
|
-/
|
|
#guard_msgs in
|
|
private def foo := 1
|
|
|
|
-- `private` inside `public section` should not warn
|
|
public section
|
|
#guard_msgs in
|
|
private def bar := 2
|
|
end
|
|
|
|
-- no modifier should not warn
|
|
#guard_msgs in
|
|
def baz := 3
|
|
|
|
-- `public` outside `public section` in a module should not warn
|
|
#guard_msgs in
|
|
set_option linter.missingDocs false in
|
|
public def qux := 4
|
|
|
|
-- `public` inside `public section` should warn
|
|
public section
|
|
/--
|
|
warning: `public` is the default visibility inside a `public section`; the modifier has no effect
|
|
|
|
Note: This linter can be disabled with `set_option linter.redundantVisibility false`
|
|
-/
|
|
#guard_msgs in
|
|
set_option linter.missingDocs false in
|
|
public def qux2 := 5
|
|
end
|
|
|
|
-- disabling the linter should suppress the warning
|
|
#guard_msgs in
|
|
set_option linter.redundantVisibility false in
|
|
private def quux := 6
|
|
|
|
-- `private` on a theorem should also warn
|
|
/--
|
|
warning: `private` has no effect in a `module` file outside `public section`; declarations are already `private` by default
|
|
|
|
Note: This linter can be disabled with `set_option linter.redundantVisibility false`
|
|
-/
|
|
#guard_msgs in
|
|
private theorem thm : True := trivial
|