We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c889785 commit 03ee6e8Copy full SHA for 03ee6e8
1 file changed
Mathlib/Tactic/Linter/FlexibleLinter.lean
@@ -457,7 +457,7 @@ def flexibleLinter : Linter where run := withSetOptionIn fun _stx => do
457
stains := new
458
459
for (s, stainStx, d) in msgs do
460
- let stainStr := (stainStx.reprint.getD s!"{stainStx}").trim
+ let stainStr := (stainStx.reprint.getD s!"{stainStx}").trimAscii
461
let msg := match stainStx.getKind with
462
| ``Lean.Parser.Tactic.simp =>
463
m!"'{stainStr}' is a flexible tactic modifying '{d}'. \
0 commit comments