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 lean2md (Seasawher) #123
• 2a6baee: fix mdgen version and restore lake run build command (Seasawher) #123
• 86d6cb2: update mdgen version (Seasawher) #123
• 98b06f9: fix build command (Seasawher) #125
• e00f797: Merge branch 'master' into mdbook (Seasawher) #121
• 468219c: delete markdown files, which are generated by mdgen (Seasawher) #121
• fbc732b: update gitignore file (Seasawher) #121
• c753cff: Merge branch 'leanprover-community:master' into master (Kitamado) #121
• 8b8b7fa: modify deploy workflow using mdgen (Seasawher) #121
• 57a83f9: add github badge to book (Seasawher) #121
• 71dd66d: modify workflow: don't deploy from non-master branch (Seasawher) #121
• e112e5f: Run CI on PRs that come from forks leanprover-community#107 (Seasawher) #127
• 8ca4674: move SUMMARY to repo root (Seasawher) #130
• ba71641: use SUMMARY for pandoc (Seasawher) #130
• 3ef475b: bug fix: invalid runCmd arguments (leanprover-community#134) (Kitamado) #134
• 2683f9a: fix issue on mdbook config (Seasawher) #137
• 4182a7f: use lake run build (Seasawher) #137
• 4988633: hide draft pages (Seasawher) #137
• 06d8d3f: update Lean and mdgen (Seasawher) #131
• ad53e6f: fix typo in MetaM chapter (Seasawher) #131
• e2f2432: Erase errors in code examples in lean\main. (Seasawher) #131
• bc380f5: format code: trim whitespace, add annotation (Seasawher) #131
• 18ed517: import Std (Seasawher) #131
• cc108fa: erase errors in exercise 2/ch5 (Seasawher) #131
• 06f48bf: add description of #check_failure (Seasawher) #131
• 0b92cde: setup workflow to run CI (Seasawher) #131
• 75f8967: added subsections to make it easier to eyeball content (Yuri de Wit) #142
• 559576b: Improves wording in 06_macros.lean (adomasbaliuka) #143
• 26651b8: Removes accidentally included character (adomasbaliuka) #143
• ca8dfad: Removes repeated "a" (determiner) (adomasbaliuka) #143
• cf2787d: Fixs typos in 03 Expressions (adomasbaliuka) #144
• 8390a98: Fix for typo in custom tactic example (Krishna Padmasola) #145
• f14102f: Update copied check output to corrected universe levels (Adomas Baliuka) #144