Zulip Chat Archive

Stream: general

Topic: brackets and `by`


Kevin Buzzard (Mar 31 2020 at 14:56):

λ x hx ε , x, hx, le_of_lt (by rwa [sub_self, abs_zero])
λ x hx ε , x, hx, le_of_lt by rwa [sub_self, abs_zero]
λ x hx ε , 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 (Mar 31 2020 at 17:40):

Try $ before by

Yury G. Kudryashov (Mar 31 2020 at 17:40):

Though it will become as long as the first one.

Kevin Buzzard (Mar 31 2020 at 17:43):

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

Reid Barton (Mar 31 2020 at 17:45):

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

Reid Barton (Mar 31 2020 at 17:46):

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

Reid Barton (Mar 31 2020 at 17:46):

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

Reid Barton (Mar 31 2020 at 17:46):

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

Kevin Buzzard (Mar 31 2020 at 17:47):

Works with the $, unsurprisingly.

Joe Hendrix (Apr 01 2020 at 07:35):

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 (Apr 01 2020 at 07:36):

\lam and \forall have the same problem

Joe Hendrix (Apr 01 2020 at 07:37):

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


Last updated: Dec 20 2023 at 11:08 UTC