Missing space in pp ouput for ∑ .. with ..

Stream: mathlib4

[Michael Stoll]

Just noticed the following.

import Mathlib

-- ∑ n ∈ Finset.range 5with Even n, 0 : ℕ
#check ∑ n ∈ Finset.range 5 with Even n, 0

The pretty-printer does not put a space before with when a numeral precedes it. (It does when I replace 5 by a variable, though.) So it does round-trip, but it still looks ugly.

[Yaël Dillies]

Oh, sounds like an issue for me. Will investigate

[Damiano Testa]

Maybe just adding a space before with in

syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term

here suffices?

[Bhavik Mehta]

Or ppSpace, perhaps?