using mdgen instead of lean2md

[Seasawher]

resolve #122

@arthurpaulino Replacing lean2md with mdgen does not seem to break the markdown file. However, the contents of the files in the lean directory are different from the contents of the files in the md directory, resulting in a large number of diffs. What should I do?

Should the contents of the lean directory be respected or the md directory?

[Seasawher]

By the way, since the contents of the md directory can be generated from the lean directory, there is no need to version control the md directory. If you need a human-readable format, you can host it on the web using mdbook. see #121

[Julian]

Thanks! This looks pretty good to me! I didn't try running mdgen yet, but I'll do that.

As for

By the way, since the contents of the md directory can be generated from the lean directory, there is no need to version control the md directory. If you need a human-readable format, you can host it on the web using mdbook. see https://github.com/leanprover-community/lean4-metaprogramming-book/pull/121

That sounds good to me as well, will have a look at that PR.

[Seasawher]

@Julian I have made corrections to the points you pointed out.

[Julian]

This looks good I think! Let's merge and see how it goes. Thanks!