Stream: new members
Topic: Lean not compiling
Ashvni Narayanan (Jan 12 2021 at 12:52):
Neither of the files are compiling, what can I do?
Any help is appreciated, thank you!
Reid Barton (Jan 12 2021 at 12:58):
There's no module
ring_theory.algebra in mathlib (I think there used to be), so maybe just delete that import.
Ashvni Narayanan (Jan 12 2021 at 13:54):
Thank you, I did that. It isn't compiling though..
Anne Baanen (Jan 12 2021 at 14:05):
Could you be a bit more specific? Is the orange bar on the left of the code not going away, or does
lean --make number_field.lean give an error?
Ashvni Narayanan (Jan 12 2021 at 14:11):
I restarted VS Code, and it seems to be working alright now. Thank you!
Last updated: May 14 2021 at 00:42 UTC