brackets and `by`

Stream: general

[Kevin Buzzard]

λ x hx ε hε, ⟨x, hx, le_of_lt (by rwa [sub_self, abs_zero])⟩
λ x hx ε hε, ⟨x, hx, le_of_lt by rwa [sub_self, abs_zero]⟩
λ x hx ε hε, ⟨x, hx, le_of_lt begin rwa [sub_self, abs_zero] end⟩

Top and bottom one work, middle one doesn't. Middle one is the shortest :-(

[Yury G. Kudryashov]

Try $ before by

[Yury G. Kudryashov]

Though it will become as long as the first one.

[Kevin Buzzard]

How come I don't need the $ for begin end though?

[Reid Barton]

Because that's the way the parser is defined? :upside_down:

[Reid Barton]

I guess begin and end already behave something like a matching pair of parentheses

[Reid Barton]

while by doesn't come along with a matching end token

[Reid Barton]

I don't know if that's really the reason though

[Kevin Buzzard]

Works with the $, unsurprisingly.

[Joe Hendrix]

I haven't looked at the lean grammar, but as by is a keyword is should be possible to make it bind to the right with higher priority and have the middle one work.

[Mario Carneiro]

\lam and \forall have the same problem

[Joe Hendrix]

I find the top version more clear personally, but I also think it would make sense for by to bind to the right.