Zulip Chat Archive

Stream: general

Topic: parser fun


view this post on Zulip Patrick Massot (Apr 24 2020 at 16:28):

Did you ever notice the space in #check nat is optional?

view this post on Zulip Floris van Doorn (Apr 24 2020 at 16:36):

Clearly a bug with the syntax highlighting of #checknat.

view this post on Zulip Patrick Massot (Apr 24 2020 at 16:39):

Yes, Lean is more lenient than the VScode plugin syntax highlighting...

view this post on Zulip Patrick Massot (Apr 24 2020 at 16:40):

Of course there is nothing specific to nat here. You can check other things.

view this post on Zulip Gabriel Ebner (Apr 24 2020 at 17:03):

Oh wow, this approach generalizes to other commands as well:

#printnat
#eval0

view this post on Zulip Patrick Massot (Apr 24 2020 at 17:04):

Unlocking mysteries of Lean...

view this post on Zulip Bryan Gin-ge Chen (Apr 24 2020 at 17:05):

I'd noticed the #eval0 example but I had no idea we could put nat there...

view this post on Zulip Kenny Lau (Apr 24 2020 at 17:05):

what if I define a user-command #chec

view this post on Zulip Patrick Massot (Apr 24 2020 at 17:06):

We said Lean is white-space sensitive only in import, right?

view this post on Zulip Patrick Massot (Apr 24 2020 at 17:06):

Why are we using all those white spaces?

view this post on Zulip Patrick Massot (Jul 09 2020 at 19:48):

With all the spaces we saved at the beginning of this thread, did you know we could do things like:

#check @ nat.rec

Combining both tricks:

#check@    nat.rec

view this post on Zulip Alex J. Best (Jul 09 2020 at 19:58):

We should use

example (n : ) (f :     ) : f 101n = 0 := sorry

more too, gotta reduce those git download times.

view this post on Zulip Johan Commelin (Jul 09 2020 at 20:22):

You mean

example(n:)(f:ℕ→ℕ→ℕ):f 101n=0:=sorry

view this post on Zulip Alex J. Best (Jul 09 2020 at 20:24):

Haha yes but then maybe people would miss the trick :wink:

view this post on Zulip Patrick Massot (Jul 09 2020 at 20:28):

Reminds me of good ol' \frac12...


Last updated: May 10 2021 at 00:31 UTC