mk-exercise: tool to extract exercises for lean text book

Stream: general

[Asei Inoue]

When writing a textbook in Lean, it is difficult to manage exercises. It would be a spoiler to write down all the answers, and correctness cannot be guaranteed if the answers are not included.

Several people have so far created tools to erase answer parts to solve this problem. (see: glimps of lean, compfiles, ... )

I have made a tool in Lean to solve this problem.

https://github.com/Seasawher/mk-exercise

Thanks.

[Bulhwi Cha]

Thank you for creating this tool! I'll use this to write a Lean book.