Zulip Chat Archive
Stream: general
Topic: Lean3 Example Error
Junaid Ahmed Mohammed (Apr 02 2023 at 17:18):
Infinitude of primes, image.png
Ruben Van de Velde (Apr 02 2023 at 17:19):
That's not lean 4 code
Junaid Ahmed Mohammed (Apr 02 2023 at 17:20):
What is it then?
Alex J. Best (Apr 02 2023 at 17:23):
Lean version 3 code. Lean 4 is currently under development, though there is already a lot of material out there for it (e.g https://leanprover.github.io/theorem_proving_in_lean4/, https://leanprover.github.io/lean4/doc/whatIsLean.html) just not that video
Junaid Ahmed Mohammed (Apr 02 2023 at 17:26):
Thank you for the info
It helps
Notification Bot (Apr 02 2023 at 17:33):
Junaid Ahmed Mohammed has marked this topic as resolved.
Notification Bot (Apr 02 2023 at 17:33):
Junaid Ahmed Mohammed has marked this topic as unresolved.
Junaid Ahmed Mohammed (Apr 02 2023 at 17:34):
I dont see any update on lean infoview
Junaid Ahmed Mohammed (Apr 02 2023 at 17:35):
Junaid Ahmed Mohammed (Apr 02 2023 at 17:38):
Expecting
image.png
Kevin Buzzard (Apr 02 2023 at 17:51):
You can't just run lean on a file, the file needs to be part of a correctly formatted lean project.
Junaid Ahmed Mohammed (Apr 02 2023 at 18:00):
is there a link or tutorial for setting up the lean project?
Alex J. Best (Apr 02 2023 at 18:03):
https://leanprover-community.github.io/install/project.html
Junaid Ahmed Mohammed (Apr 02 2023 at 18:15):
Thank you
Notification Bot (Apr 02 2023 at 18:15):
Junaid Ahmed Mohammed has marked this topic as resolved.
Notification Bot (Apr 28 2023 at 16:20):
Chris Hughes has marked this topic as unresolved.
Last updated: Dec 20 2023 at 11:08 UTC