Exercises for Ch.Syntax & Ch.Elaboration

leanprover-community / lean4-metaprogramming-book

Apache License 2.0

211 stars 50 forks source link

Closed lakesare closed 1 year ago

lakesare commented 1 year ago

[Based on #84]

Created exercises & solutions for Ch.Syntax
Created exercises & solutions for Ch.Elaboration
Fixed missing code blocks in Ch.MetaM exercises
in /solutions we used to have abridged descriptions of the exercise text - removed that, let's just have the exercise number

lakesare commented 1 year ago

@arthurpaulino, I think it's good to merge.

arthurpaulino commented 1 year ago

Amazing, thank you!