Lean functionality is exposed in the UI via the universal quantifier at the top right of VS code.
Consider copying the MIL folder, containing key examples, so you can tinker with the example code.
MIL = Mathematics in Lean.
When you download the MIL, you will see a flurry of activity in your Output Console in VS Code. This will include reams of stuff relating to "Fetching Mathlib build artifact cache" and thousands of file downloads.
You will also see the incantation "lake build" which is the primary build command in the Lean build system.
Advice on how to work through the MIL textbook from the official website - "working through the exercises is central to the experience".
Note: when reading Lean files in VS code turn off Unicode character highlighting (Control-, to get into settings, and update Text Editor settings).
No comments:
Post a Comment