error: unknown identifier M

Stream: new members

[tsuki hao]

a.png

Does anyone know how to handle this problem

[Notification Bot]

A message was moved here from #general > Recommended font by Johan Commelin.

[Johan Commelin]

@tsuki hao Something about your setup seems broken. Let's try to debug it.

[Johan Commelin]

Can you open the mathlib project in a new VScode window? If you open a random file, will it work without errors, or do you get errors in that case as well?

[Johan Commelin]

How did you create your sadf project?

[tsuki hao]

Johan Commelin said:

tsuki hao Something about your setup seems broken. Let's try to debug it.

How should I debug it, I know very little about the operation in this area

[Scott Morrison]

@tsuki hao, please answer Johan's questions in his comment beginning "Can you open ...". He is trying to help you debug it. :-)

[tsuki hao]

Johan Commelin said:

tsuki hao Something about your setup seems broken. Let's try to debug it.

[tsuki hao]

I'm sorry I didn't see the full comment at the beginning, I can't open mathlib in a new window and any file will be wrong, I followed the instructions to create sadf in the terminal, it confuses me that I was fine yesterday use mathlib.I'm sorry I'm not very proficient in using the forum at the beginning.

[Johan Commelin]

Do you know how to use a terminal? Could you please navigate to a copy of the Mathlib repository and run lake exe cache get!?
If there are any errors, please paste them here.

[tsuki hao]

Johan Commelin said:

Do you know how to use a terminal? Could you please navigate to a copy of the Mathlib repository and run lake exe cache get!?
If there are any errors, please paste them here.

Thank you for your help. I solved this problem with the help of friends in the real world. It seems that the version of elan is not correct. Thanks again for your help.

[Johan Commelin]

@tsuki hao I'm glad your problem is now solved!