Force whitespace in notation

Stream: lean4

[Kenny Lau]

def g : Nat → Type → Type := fun n x ↦ (Fin n → x)

notation "Σ" n:arg x:arg => g n x

#check (g 0 Int) -- Σ0Int : Type

If I define a notation like this, Lean automatically deletes the whitespace between 0 and Int. Is there a way to force Lean to put the whitespace back in?

This is giving me an issue because of the new whitespace linter complaining about the extra space when I do write Σ0 Int.

[Aaron Liu]

I would say to use docs#Lean.Parser.ppSpace but that doesn't seem to be working here

[Damiano Testa]

I don't know how to get the space there with notation, but you should be able to get what you want with syntax.

[Damiano Testa]

There is a similar issue with another notation and I added the notation to the list of exceptions for the linter: you could also do that.

[Damiano Testa]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib%2FTactic%2FLinter%2FCommandStart.lean#L235

[Damiano Testa]

You could add the name of the syntax node to this list as well.

[Kenny Lau]

Damiano Testa said:

There is a similar issue with another notation and I added the notation to the list of exceptions for the linter: you could also do that.

Did syntax not work in that case?

[Damiano Testa]

I did not try it, since I was trying the get mathlib to compile with the smallest change to pre-existing code.

[Damiano Testa]

Once the linter "works", I plan to revisit the exceptions and try to iron them out, when possible.

[Robin Arnez]

Not sure if there's a better way:

def g : Nat → Type → Type := fun n x ↦ (Fin n → x)

macro "Σ " n:term:arg ppSpace x:term:arg : term => `(g $n $x)

@[app_unexpander g]
private def unexpandG : Lean.PrettyPrinter.Unexpander
  | `($_ $n $x) => `(Σ $n $x)
  | _ => throw ()

#check (g 0 Int) -- Σ 0 Int : Type