4 lines
592 B
Text
4 lines
592 B
Text
linterSuspiciousUnexpanderPatterns.lean:6:6-6:14: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
|
|
note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
|
|
linterSuspiciousUnexpanderPatterns.lean:11:6-11:15: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
|
|
note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
|