rw sytax

Stream: new members

[Michael Beeson]

 rw successor_members M at h10,

works fine although I thought it should have to be

 rw (successor_members M) at h10,

My question is, how in the world can the first version possibly actually work?

I guess it's related to the fact that

 rw successor_members  at h10,

also works. I guess the "elaborator" is able to supply the argument M in that case, because it needs an
element of class Model and there is only one such in the environment, namely M. But that still
doesn't explain the first example.

[Ruben Van de Velde]

I'm assuming it reads until it finds "at"

[Yakov Pechersky]

rw is not a function like a usual lean term, but rather, a tactic. For example, the following also works:

rw [successor_members M] at h10,

or

rw [successor_members] at h10

This is because rewrite is a tactic that takes an expression or a list of expressions. It parses the expression until some token it is aware of, like at. So successor_members M is such an expression. That's my understanding of how this tactic works, but could be mistaken.

[Reid Barton]

Right, tactics have their own parsing logic and in this context at is a keyword. It's not as though rw is a function and at is one of its arguments.