teach computer to do some stupid mathematics BOOGITY BOOGITY
- Download Lean autonomous bundle (say) from https://leanprover-community.github.io/get_started.html
- Checkout this repository when you are in folder
trylean
. Now you should have the foldertrylean/my-lean-test
- Modify the contents of
trylean.bat
to.\vscodium\VSCodium my-lean-test
- BOOGITY BOOGITY
- Run trylean.bat
- Navigate to any lean file
- BOOGITY BOOGITY