pretty printing of reverse simp attribute

Stream: lean4

[Aaron Liu]

Surely we want @[simp ←] instead of @[simp← ]?

import Mathlib.Tactic.Linter.Whitespace

set_option linter.style.whitespace true

/--
warning: extra space in the source

This part of the code
  '@[simp ←]
theorem'
should be written as
  '@[simp← ]
theorem'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
---
warning: missing space in the source

This part of the code
  '←]
theorem'
should be written as
  '@[simp← ]
theorem'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
-/
#guard_msgs in
@[simp ←]
theorem foo : 0 = id 0 := rfl

mathlib-free:

import Lean

/-- info: @[simp← ] -/
#guard_msgs in
#eval return ← Lean.PrettyPrinter.ppCategory `Lean.Parser.Term.attributes (← `(Lean.Parser.Term.attributes| @[simp ←]))

[Kim Morrison]

Issue and/or fix welcome!

[Eric Wieser]

Presumably a lot of things like this will naturally be fixed as part of the code formatter work?

[Eric Wieser]

(which is not to say we shouldn't fix them as we find them)