Zulip Chat Archive

Stream: new members

Topic: error on "import tactic.ring"

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

Bryan Gin-ge Chen (Nov 06 2019 at 05:28):

Did you follow the directions in the projects doc?

agro1986 (Nov 06 2019 at 05:31):

hmmm, let me check

agro1986 (Nov 06 2019 at 07:04):

@Bryan Gin-ge Chen It works! thanks

Last updated: Dec 20 2023 at 11:08 UTC