Zulip Chat Archive

Stream: general

Topic: brackets and `by`


view this post on Zulip 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 :-(

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 17:40):

Try $ before by

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 17:40):

Though it will become as long as the first one.

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 17:43):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 17:45):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 17:46):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 17:46):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 17:46):

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

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 17:47):

Works with the $, unsurprisingly.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 07:36):

\lam and \forall have the same problem

view this post on Zulip 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: May 09 2021 at 19:11 UTC