Changes from the Logic colloquium - Githubissues

PatrickMassot / GlimpseOfLean

An introduction to theorem proving in Lean for the impatient.

Apache License 2.0

95 stars 44 forks source link

Changes from the Logic colloquium #2

Closed fpvandoorn closed 1 year ago

fpvandoorn commented 1 year ago

Take the changes from the Logic colloquium tutorial and move them here

Notable changes:

Update README (but with a less elaborate explanation than in my repo).
Look at commit ca078782da531f4d2b44735cdf0f7c79239f8ce2 for the changes to the Lean files (which we mostly discussed)
Add two files on the metatheory of propositional logic
update mathlib
change VSCode settings (one remark: font specification removed. DejaVu sans mono is not a default font on Windows)
Add a LICENSE