Working with these activities

Follow the instructions for working on an existing project to work on these files. Specifically:

1. Navigate to the directory where you want these files to be.
2. In your terminal, run:

   git clone https://github.com/math4345/lectures.git
   

3. Enter the newly created directory:

   cd lectures
   

4. Fetch the previously built mathlib4 files:

   lake exe cache get
   

You can then launch your favorite editor. If using VS Code, type:

code .

Have fun!