CODEWITHSUNDEEP
theorem-provinglean
then999
then999

Reputation: 43

Unknown identifier 'begin' in Lean4

I've typed the following into Lean4 in VSCode:

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) :=
begin

and it tells me "unknown identifier 'begin'". When I type the end two lines down, it tells me "invalid 'end', insufficient scopes". What am I doing wrong? Did I not set Lean up properly?

Upvotes: 2

Views: 601

Answers (2)

Utensil
Utensil

Reputation: 19663

It means you have successfully installed Lean 4 which has syntax that are not fully compatible with Lean 3.

In addition to Chris' answer, by and optional done, if you are familiar with Lean 3, you might also want to check out Lean 4 survival guide for Lean 3 users which gives a pretty good overview of major differences.

Upvotes: 2

ammkrn
ammkrn

Reputation: 151

begin/end blocks are lean 3 syntax. The keyword for entering tactic mode in Lean 4 is by, as in:

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) := by sorry

There's no analog to end anymore since it now relies on white space, but there is an optional done finisher that will become an error if the goal is not in fact closed.

Even if you used lean 3 quite a bit, I would recommend skimming the manual and/or Theorem Proving in Lean/Functional Programming in Lean (see chapters 4 and 5 in the manual) since there have been significant changes and improvements.

end is still the keyword for ending sections and namespaces, which is why you're getting that error message for the end keyword.

Upvotes: 5

Related Questions