theorem

Stream: lean4

[Andrea]

I am playing with theorems but it looks like the documentation is mostly for Lean3. It seems like the syntax has changes and begin/end are not used for example. Where can I find some extensive documentation about theorems and tactics for Lean4?

[Mario Carneiro]

The new notation uses by:

example : True := by
  tac1
  tac2

[Mario Carneiro]

The most extensive documentation right now for lean 4 tactics is https://leanprover.github.io/lean4/doc/tactics.html

[Kevin Buzzard]

Lean 4 has not had a stable release yet, so it's difficult to write docs because the syntax might not even have stabilised. The name of the <= class changed a week or two ago, for example (from hasLessEq to LE).