Category Archives: Technical assistance
No errors.
Does your Lean file contain errors? Try and cut down. Continue reading
Posted in Learning Lean, Technical assistance, Uncategorized
Tagged CoCalc, error, errors, VS Code
Leave a comment
How to install mathlib and keep it up to date
Important: I deleted this post because it was out of date and causing confusion. The Lean Community now has its own website and up to date installation instructions for getting Lean and the key tool leanproject are here.
Posted in Technical assistance
6 Comments
Installing Lean (and VSCode) on Windows from scratch
THIS POST IS TWO YEARS OLD AND VERY OUT OF DATE. THE MODERN WAY TO INSTALL LEAN AND MATHLIB (UPDATED CONTINUOUSLY) IS EXPLAINED IN THE README ON THE MATHLIB GITHUB SITE: modern installation instructions for Lean The below used to … Continue reading
Posted in Technical assistance
5 Comments