Zulip Chat Archive
Stream: new members
Topic: Hello & Help!
Kristaps John Balodis (Jan 09 2021 at 07:21):
Hi! I'm excited to finally be getting my hands dirty with Lean, I've been convinced proof assistants are the future for some time, now to put theory into action!
Just working my way through the basics of the tutorial PDF and various commands seem to work fine, I'm getting an error whenever I try to import something, namely
file 'theory\set_theory' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
What can I/should I do?
Kenny Lau (Jan 09 2021 at 07:22):
what's the tutorial PDF?
Kristaps John Balodis (Jan 09 2021 at 07:22):
I mean the Theorem Proving in Lean document:
https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf
Kenny Lau (Jan 09 2021 at 07:24):
did you look at the link provided?
Kristaps John Balodis (Jan 09 2021 at 07:28):
Woops, totally missed that, thanks.
Last updated: Dec 20 2023 at 11:08 UTC