Some material for Lean 4 lectures at IISc.
Written in Bengaluru, April 2023.
See the RESOURCES file.
This is the best way; you can edit files and experiment, and you won't lose them. It's also the hardest way: it involves typing stuff in on the command line.
In brief: first install Lean 4 following the instructions here.
Then download and install this project by going to its home page on GitHub, clicking "Code" and "local", and then downloading the project onto your computer.
Pic: 
Next open a command line in the project folder, type lake exe cache get, and wait until all files are downloaded and installed and your cursor has reappeared.
Finally, open the root directory of the project folder in VS Code. You can open the files in the IIScExperiments directory (not the IIScExperiments.lean Lean file!) and these correspond to the material I was going through in lectures.
You don't need to install anything onto your computer using this method.
Just click here:
Note to self: I got gitpod working by adding the files .gitpod.yml and .docker/gitpod/Dockerfile
You don't need to install anything onto your computer using this method.
Go to the project's home page on GitHub, click "Code" and then "Codespaces" so it looks like this:
Pic: 
Then click "create codespace on main", and then wait for a few minutes. When it looks like everything has downloaded, open up the IIScExperiments directory (not the file!) and the code I've been using in the lectures should just work.
Note to self: I got codespaces working by adding the files .devcontainer/devcontainer.json and .devcontainer/Dockerfile.