Zulip Chat Archive

Stream: new members

Topic: Is there a type abbreviation? Should I use 3.X or 4?


view this post on Zulip Brian Milnes (Dec 20 2020 at 21:49):

inductive PE ..
type Path := list PE
I can't seem to find one.
Additionally, the lean3 manual seems to be hidden and thin, should I be using 4?

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 21:50):

the lean 3 manual is #tpil and is beautiful; you should not be using Lean 4 because it is not even finished (e.g. there is no tactic mode).

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:51):

It isn't quite true there is no tactic mode. You mean no serious editor support.

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 21:51):

I tried it the other day and begin end didn't work. Did I do something wrong?

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 21:51):

(I was using emacs)

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:51):

Yes, you are a so-called "begin-end or brace lover" or something like that. This is old-fashioned.

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 21:52):

Oh!

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:52):

https://leanprover.github.io/lean4/doc/tactics.html#begin-end-lovers

view this post on Zulip Patrick Massot (Dec 20 2020 at 21:52):

(of course the beginning of that webpage is also relevant)


Last updated: May 16 2021 at 05:21 UTC