Closed yangky11 closed 1 year ago
Hi @yangky11! The changes need to be made in the original Lean files. The markdown files are generated automatically.
For more info, read https://github.com/arthurpaulino/lean4-metaprogramming-book#contributing
I fixed that list issue in this PR: https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/87/files#diff-6abc89e33f9cc7c0f7eb28848918984968986f78fdbef61061e760dd1ec043e9.
Hi @yangky11! The changes need to be made in the original Lean files. The markdown files are generated automatically.
For more info, read https://github.com/arthurpaulino/lean4-metaprogramming-book#contributing