Style linter for ←

Stream: PR reviews

[Robert Maxton]

Is it intended that the "space after ←" linter should trigger on set lines like

set x' := ofDirectSum x with ←x'_def

That seems odd to me, since I associate those with the ← arrows used for backward rewrites in rw syntax and those are never spaced.

[Ruben Van de Velde]

Backward arrows in rw are always spaced in mathlib

[Ruben Van de Velde]

(I think this was a bad choice in the mathport output, but that's where we are)

[Robert Maxton]

Ew.

[Robert Maxton]

Alright, I guess...