.lake\packages\mathlib\Mathlib\Tactic\Linter\Style.lean introduces a new defsWithUnderscore linter,
The most problematic issue is informal_lemma which elaborates to a def, probably need to include @[nolint defsWithUnderscore]
_physlib-suffixed instances are also flagged, the linter identifies _mathlib ones but not physlib
there's also some meta declarations e.g. semiformal_result, Sorryful_attr, Pseudo_attr
the linter exempts _1 and _2 but not _3 and _4 in Physlib.Mathematics.DataStructures.FourTree.Basic
linter turned off for now but should be fixed
Originally posted by @zhikaip in #1130 (comment)
.lake\packages\mathlib\Mathlib\Tactic\Linter\Style.lean introduces a new
defsWithUnderscorelinter,The most problematic issue is
informal_lemmawhich elaborates to adef, probably need to include@[nolint defsWithUnderscore]_physlib-suffixed instances are also flagged, the linter identifies
_mathlibones but not physlibthere's also some meta declarations e.g.
semiformal_result,Sorryful_attr,Pseudo_attrthe linter exempts
_1and_2but not_3and_4in Physlib.Mathematics.DataStructures.FourTree.Basiclinter turned off for now but should be fixed
Originally posted by @zhikaip in #1130 (comment)