Zulip Chat Archive

Stream: new members

Topic: Hello & Help!


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 09 2021 at 07:22):

what's the tutorial PDF?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 09 2021 at 07:24):

did you look at the link provided?

view this post on Zulip Kristaps John Balodis (Jan 09 2021 at 07:28):

Woops, totally missed that, thanks.


Last updated: May 08 2021 at 19:11 UTC