learnlean

I had a frustrating time with Lean today. 

Did some more exercises, but then the Lean plugin died in VSCode after restarting it to fix a UI issue and I haven't managed to resolve it yet. I asked on Zulip where there seems to be a helpful community.

I then took a peak at the solution for the next exercise and it uses a theorem that hasn't been introduced yet, but the exercise said to only use theorems that have been introduced. 🤷 

https://github.com/leanprover-community/mathematics_in_lean/commit/61e9eca92c9c4400e6586b32d274e99db706570a

Sat down to get some Lean done before the day starts. Good news is that that the VSCode plugin works again. Turns out it was the old have to accept Xcode CLI tools license after an update issues. After this the toolchain failed to build the mathlib so I had to reinstall that too, but now it all seems to work again. 🙏 No time for proofs though