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

Stream: new members

[Brian Milnes]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(I was using emacs)

[Patrick Massot]

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

[Kevin Buzzard]

Oh!

[Patrick Massot]

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

[Patrick Massot]

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