I'm using the Lean computer proof assistant on my Mac.
I tried to import data.nat.basic from lean's documentation, just like this:
I get this:
could not resolve import: data.nat.basic All Messages (2) Topologic.lean:1:0 file 'data/nat/basic' 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 Topologic.lean:6:1 invalid import: data.nat.basic could not resolve import: data.nat.basic
Evidently I missed the memo on one of the relevant installations and it means I can't use math lib. Basically I want to be able to use hash maps and lists from lean's math lib.
Can anyone direct me towards a tutorial for installing the relevant files for lists and hash sets? I am going to guess this involves installing math lib packages.
I've never actually worked with GitHub before so I would be grateful if someone had a link to a complete set of instructions.
Further, it seems like the instructions for Mathlib installation don't work- I get an error message printed in the comments below.