In the VSCode editor, I entered this Lean4 code:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) :=
beginand got "unknown identifier 'begin'". Adding end three lines below gives "invalid 'end', insufficient scopes". What have I done wrong? Is my Lean installation incorrect?
The begin/end block notation belongs to lean 3. To start tactic mode with Lean 4, use the keyword by, for example:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorryThere is no corresponding end now because white space determines the scope, although an optional final done produces an error when a goal remains open.
Even with substantial lean 3 experience, I'd suggest looking through the manual (https://lean-lang.org/lean4/doc/) and/or Theorem Proving in Lean/Functional Programming in Lean (chapters 4 and 5 of the manual), given the considerable improvements and changes.
The end keyword still closes sections and namespaces, explaining the diagnostic you see when using end here.
It indicates a successful Lean 4 installation, whose syntax isn't entirely compatible with Lean 3.
Alongside hkr's answer about by and optional done, anyone who knows Lean 3 may find the Lean 4 survival guide for Lean 3 users (https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users) useful, as it provides a good account of the main differences.
I'm a functional programming beginner, trying to create a function which accepts values in a list (whose length isn't fixed)…
The last year I consulted JavaScript documentation was 1996. I'd like an educational course covering the “essential JavaScrip…
Lots of go examples begin with : The GOPATH I use: Where are main and the fmt module stored?
