parser fun

Stream: general

[Patrick Massot]

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

[Floris van Doorn]

Clearly a bug with the syntax highlighting of #checknat.

[Patrick Massot]

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

[Patrick Massot]

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

[Gabriel Ebner]

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

#printnat
#eval0

[Patrick Massot]

Unlocking mysteries of Lean...

[Bryan Gin-ge Chen]

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

[Kenny Lau]

what if I define a user-command #chec

[Patrick Massot]

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

[Patrick Massot]

Why are we using all those white spaces?

[Patrick Massot]

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

[Alex J. Best]

We should use

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

more too, gotta reduce those git download times.

[Johan Commelin]

You mean

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

[Alex J. Best]

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

[Patrick Massot]

Reminds me of good ol' \frac12...