keywords changed from lean 3

Stream: lean4

[Kevin Lacker]

Does lean4 change the meaning of the keywords lemma, begin, and end? They aren't mentioned in the "significant changes" document at https://leanprover.github.io/lean4/doc/lean3changes.html but when I try out some simple stuff in lean 4 it does not seem like they work any more.

[Patrick Massot]

They are gone.

[Patrick Massot]

You can use theorem instead of lemma, use by instead of begin and forget about end.

[Kevin Lacker]

ok cool. it would be handy to have a list of all lean 3 keywords that have been renamed or removed from lean 4

[Patrick Massot]

I guess you can try to open a PR adding this to the page you were looking at. Polite documentation PRs are rather welcome.

[Kevin Lacker]

I was thinking about it, I just hesitate to try to document lean 4 when I know so little about it

[Kevin Lacker]

here's a similar issue, although one notch more complicated - I believe in lean 3 the trivial tactic would prove p -> p. now it does not seem to. is that a change in how things work and I should use another tactic there, or am I misremembering?

[Kevin Buzzard]

trivial doesn't appear to prove p -> p in Lean 3.

[Yaël Dillies]

lemma is most definitely not gone. I've been using it myself.

[Kevin Buzzard]

It's gone in core Lean -- it was re-added in mathlib.

[Kevin Buzzard]

I think it is so cool that Lean 4 is so flexible that with just a few lines of code you can do this. I am still really excited by those changes in Lean 4. It took me a while to understand the significance -- at some point I was moaning to Leo about how I couldn't do X any more and he just said "sure you can do X, you can just do it yourself -- that's the point"