Metaprogramming in Lean 4

Features

• prefix filenames with numbers, so that they are sorted correctly #104 (Johan Commelin)
• prefix filenames with numbers, so that they are sorted correctly #106 (Johan Commelin)

Bug Fixes

• intro: fix counterexample #102 (Johan Commelin)
• correct some typos, following Grammarly #106 (Johan Commelin)
• correct some typos, following Grammarly (2) #109 (Johan Commelin)
• broken link #129 (Seasawher)
• typo #130 (Seasawher)
• workflow duplication problem #130 (Seasawher)
• missing solutions in mdbook #130 (Seasawher)
• pandoc command in CI #137 (Seasawher)
• command to build PDF #137 (Seasawher)
• command to build PDF #137 (Seasawher)

Tests

• setup deploy workflow #121 (Seasawher)

Chores

• switch main/03_expressions.lean to semantic linebreaks (leanprover-community#110) #110 (Johan Commelin)

Commits

• clarify bvar/fvar terminology (leanprover-community#82) #82 (Jannis Limperg)
• 2a2dcb4: Update Lean to nightly-2022-12-16 (leanprover-community#83) (Jannis Limperg) #83
• c0ed4ab: Adding exercises (leanprover-community#85) (Evgenia Karunus) #85
• 520987f: Enable pdf generation in prs; fix chapter structure (leanprover-community#86) (Evgenia Karunus) #86
• 70a8eba: mention FPIL and add note about how code snipets aren't self-contained (Arthur Paulino)
• 4a5512a: fix typo (leanprover-community#88) (Kevin Buzzard) #88
• 52d1bed: fix typo on lean file (Arthur Paulino)
• 7fbf966: Exercises for Ch.Syntax & Ch.Elaboration (leanprover-community#87) (Evgenia Karunus) #87
• e00cf56: Quick fixes for pdf lists to render fine (leanprover-community#90) (Evgenia Karunus) #90
• better intro (leanprover-community#91) #91 (Jannis Limperg)
• 59b8627: Fix typos (leanprover-community#92) (leanprover-community#93) (Arthur Paulino) #93
• 1c52cdb: run viper_build (Arthur Paulino)
• d6a227a: Fix typos (leanprover-community#94) (Tomaz Gomes Mascarenhas) #94
• a1ddea2: Update intro.lean (leanprover-community#97) (Samuel) #97
• f1b2fab: Update intro.md (leanprover-community#96) (Samuel) #96
• eb684e0: Init (Evgenia Karunus) #98
• f26176f: Readme.md - add solutions link to the outline (Evgenia Karunus) #98
• e717be1: Generate .md files + better formatting (Evgenia Karunus) #98
• 4fc5d41: Add Ch.Overview (leanprover-community#99) (Evgenia Karunus) #99
• 2b6d604: apt update is needed in case of package indices being out of date (Julian Berman) #105
• cb42ec2: Remove isLeanOnly from the lakefile. (Julian Berman) #108
• f0e2a99: Use python3 not python as the binary name in the lakefile. (Julian Berman) #108
• b4f7156: Regenerate the markdown pages via lake run build. (Julian Berman) #104
• 380ac50: And now update the TOC for the new filenames. (Julian Berman) #104
• 78af27e: Two minor lakefile tweaks (leanprover-community#108) (Julian Berman) #108
• 365f14d: missing space (Martin Dvořák) #103
• 1656f69: Update lean/main/intro.lean (Johan Commelin) #106
• 36ad26c: Two minor lakefile tweaks (leanprover-community#108) (Julian Berman) #106
• a1244c1: Regenerate the markdown pages via lake run build. (Julian Berman) #106
• 3ca6e52: And now update the TOC for the new filenames. (Julian Berman) #106
• 5c4960a: process review comments (Johan Commelin) #106
• adecea6: Merge branch 'master' into 01-grammarly (Johan Commelin) #106
• e60e547: Apply suggestions from code review (Johan Commelin) #109
• 773195a: Merge branch 'master' into 02-grammarly (Johan Commelin) #109
• 56ab3b4: Merge (Evgenia Karunus) #98
• d6466a8: Build files (Evgenia Karunus) #98
• dc3f42a: Remove last 2 exercises (Evgenia Karunus) #98
• 3a76461: Merge remote-tracking branch 'origin/02-grammarly' (Julian Berman) #109
• bba6f99: Merge remote-tracking branch 'origin/assert-type' (Julian Berman) #102
• b84860c: No default target in lakefile (tydeu) #120
• eea73c5: Enable mdbook to build html (Seasawher) #121
• 838111e: set up the deploy workflow (Seasawher) #121
• 8459f6b: update lean version to v4.4.0 (Seasawher) #123
• 85fd99d: Merge branch 'update-to-v4.4.0' into mdgen (Seasawher) #123
• 950c47d: install mdgen (Seasawher) #123
• 6408ed4: generate markdown files by mdgen (Seasawher) #123
• 6695ec2: delete description about ...