Pretty printing instances in `omit`

Stream: lean4

[Damiano Testa]

I found the pretty-printed spaces in the omits below a bit strange. Should the instance binders be separated by spaces as well?

import Lean.Elab.Command
open Lean

-- no spaces around `[` and `]`
/-- info: omit a✝ b✝[A✝][B✝] -/
#guard_msgs in
run_cmd
  logInfo (← `(omit a b [A] [B]))

-- here there the spaces are present
/-- info: variable [A✝] [B✝] -/
#guard_msgs in
run_cmd
  logInfo (← `(variable [A] [B]))

[Eric Wieser]

lean4#8169

[Damiano Testa]

Thanks Eric!

[Damiano Testa]

I think that include already "worked", since it only takes identifiers (right?) and those are separated by spaces anyway.

[Eric Wieser]

Sure, but my change also (deliberately) makes

variable (or whatever : Nat)
include
or
omit
whatever

a syntax error, and forces you to write

variable (or whatever : Nat)

include
  or
omit
  whatever

[Mario Carneiro]

Damiano Testa said:

I think that include already "worked", since it only takes identifiers (right?) and those are separated by spaces anyway.

There are many examples of this (flawed) reasoning in lean parsers, I tried to fix most of them a while back. It's not robust reasoning exactly because anywhere an identifier can appear you can get a dagger after it (as in your example!) and daggers are not identifier characters. It's much better to actually put a space if you want a space

[Damiano Testa]

I agree with all the discussion here: the quotation around "worked" were an attempt at making a joke, not aiming at modifying Eric's PR! :smile: