Metaprogramming in Lean 4

Bug Fixes

• 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)

Commits

• 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
• ffd9266: merge upstream (Jeremy Toh)