Stream: general

Topic: brackets and by

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

λ 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 :-(

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: May 09 2021 at 19:11 UTC