How to add a path in Lean exactly?

Stream: lean4

[Jenny Kim]

Could anyone please help with the following questions:

How to add a path exactly, or how to fix the error that "file 'tactic\suggest' not found in the search path" exactly?

Thanks a lot!

[Arthur Paulino]

Are you trying to use mathlib? You need Lean 3 for that (I'm assuming you installed Lean 4 because you're asking in the Lean 4 stream)

[Jenny Kim]

Arthur Paulino said:

Are you trying to use mathlib? You need Lean 3 for that (I'm assuming you installed Lean 4 because you're asking in the Lean 4 stream)

Yes, but there doesn't seem to be a Lean 3 chat group. However, do you know How to add a path exactly, or how to fix the error that "file 'tactic\suggest' not found in the search path" exactly? Thanks a lot!

[Arthur Paulino]

Sorry, it's been a while since I haven't used Lean 3. I believe you're not in a Lean 3 project that properly uses mathlib as a dependency. Are you trying to import tactic.suggest?

[Arthur Paulino]

I think you will have better luck in the #new members stream

[Mario Carneiro]

Lean 3 is basically all the streams except for #lean4 and #mathlib4