lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Adding exercises

Open lakesare opened this issue 1 year ago • 1 comments

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:

image

and end with:

image

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?

lakesare avatar Jan 02 '23 06:01 lakesare