## Stream: new members

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

#### 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?

#### 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).

#### Patrick Massot (Dec 20 2020 at 21:51):

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

#### 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?

#### Kevin Buzzard (Dec 20 2020 at 21:51):

(I was using emacs)

#### 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.

Oh!

#### Patrick Massot (Dec 20 2020 at 21:52):

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

#### 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