installing mathlib

Stream: new members

[Chris M]

I just tried the "Mathematics in Lean" tutorial, and copied this command into my VSCode:
import data.nat.parity tactic. It gave me the following error:

test11.lean:1:0: error
file 'data\nat\parity' not found in the LEAN_PATH

Does this mean I haven't installed mathlib during my installation of Lean? (note that Lean otherwise has been working fine for me for a long time)

[Chris M]

Somehow I accidentally changed the title of lots of previous messages to "installing mathlib".

[Bryan Gin-ge Chen]

Chris M said:

Somehow I accidentally changed the title of lots of previous messages to "installing mathlib".

I think you just added your messages to an already existing thread.

[Bryan Gin-ge Chen]

Chris M said:

I just tried the "Mathematics in Lean" tutorial, and copied this command into my VSCode:
import data.nat.parity tactic. It gave me the following error:

test11.lean:1:0: error
file 'data\nat\parity' not found in the LEAN_PATH

Does this mean I haven't installed mathlib during my installation of Lean? (note that Lean otherwise has been working fine for me for a long time)

Try re-running leanproject get-mathlib-cache?