In this repository, you'll find Lean files for my guest lecture at AUB. These materials are based off of my course CS1715 and Heather Macbeth's metaprogramming tutorial.
This repository is a Lean project. There are some basic steps you should take at the beginning to set it up. These only need to be done once.
We assume that you have installed:
gitlean(viaelan)- VSCode and the Lean extension
following our course setup instructions.
To set up this project, run:
git clone https://github.com/robertylewis/aub-guest-lecture.git
cd aub-guest-lecture
lake exe cache getWhen you open VSCode, make sure that you use the Open Folder feature
to open the entire aub-guest-lecture directory,
instead of opening individual files.
The easiest way to do this is from the command line:
cd aub-guest-lecture
code .But File -> Open Folder... works fine too.
If you are using GitHub Codespaces, you can ignore all of the above. Open your codespace and get to work; all of these setup steps are done for you!