Adding exercises

[lakesare]

Progress

• [ ] Introduction
• [ ] Overview
• [x] Expressions
• [x] MetaM
  • [x] Metavariables
  • [x] Computation
  • [x] Constructing Epxressions
  • [x] Backtracking
• [x] Syntax
• [ ] Macros
• [x] Elaboration
• [ ] DSLs
• [x] Tactics

---

Initial issue

I'm going through the book chapter by chapter, and finding it beneficial to improvise ~10 exercises per each subchapter, starting from easy ones and ending up with something more intense.

For example, exercises for the MetaM#Constructing Expressions subchapter start with:

and end with:

Would the PRs gradually adding exercises to the end of the chapter and solutions (in the end of the book) be welcome, do you think it could be a good idea?

[arthurpaulino]

It would definitely be a honorable effort of great help! Please don't forget to add yourself as an author if you do so 👍🏼