Zulip Chat Archive

Stream: new members

Topic: error on "import tactic.ring"


view this post on Zulip agro1986 (Nov 06 2019 at 05:28):

Hi. I tried installing mathlib on MacOS based on the instruction here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md

However when I typed import tactic.ring on my first line (in VS Code), the interpreter gives me

file 'tactic/ring' not found in the LEAN_PATH

invalid import: tactic.ring
could not resolve import: tactic.ring

Can anyone point me to the right direction? Thanks

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2019 at 05:28):

Did you follow the directions in the projects doc?

view this post on Zulip agro1986 (Nov 06 2019 at 05:31):

hmmm, let me check

view this post on Zulip agro1986 (Nov 06 2019 at 07:04):

@Bryan Gin-ge Chen It works! thanks


Last updated: May 10 2021 at 00:31 UTC