[Merged by Bors] - fix: space after separator

[digama0]

Fixes leanprover-community/mathport#122 (comment)

[gebner]

bors r+

[gebner]

I think we had a similar problem for binder notation, and there I added the space in mathport (addSpaceBeforeBinders). It shouldn't make a difference though, the notation3 command is temporary after all.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build

[digama0]

It shouldn't make a difference though, the notation3 command is temporary after all.

I'm not so sure about that. I mean yes, the name notation3 is terrible, but it does things in one line that you currently can't do with lean 4 builtin stuff. (If you could, I would have used that in mathport instead of making a custom notation.) You need to set up syntax, elab and delab, and for binders and fold notations this currently involves writing a small program, which seems like a bad tradeoff for people introducing e.g. vec_notation or big_operators.

[gebner]

Completely agreed that we need a higher-level API to declare custom binders, etc. I'm just not convinced that the Lean 3 notation command is the ideal API to base this on, as it is famously hard to learn.