Closed Seasawher closed 6 months ago
resolve https://github.com/leanprover-community/lean4-metaprogramming-book/issues/128#issuecomment-1890821487
This PR also includes following small fixes:
this PR also resolve #126
use SUMMARY.md for both mdbook and pandoc
resolve https://github.com/leanprover-community/lean4-metaprogramming-book/issues/128#issuecomment-1890821487
This PR also includes following small fixes: