Changing the notation for no_index

Stream: lean4

[Eric Wieser]

In #lean4 > simproc for Fin, @Bhavik Mehta and I discovered that there are some placed in mathlib where no_index is used incorrectly.

Can we change its syntax to make this much harder to do accidentally? Right now

#check id no_index id 1

is legal, and means id (no_index id) 1. This is particularly confusing give other inline keywords like unsafe have different parsing rules here.

Can the notation either be changed to match unsafe (so that no_index f x means no_index (f x)) or changed to no_index(f x) such that the parens are required?

[Kim Morrison]

@Eric Wieser, would you mind creating an issue for this?