leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
211 stars 50 forks source link

`syntax.lean`: minor details and typo/grammar/punctuation fixes #48

Closed rish987 closed 2 years ago

rish987 commented 2 years ago

Just some minor fixes and some details that I thought would be helpful (of course let me know if you disagree on anything). I have some changes to the later chapters as well, will make separate PRs for those after I take a look at the recent additions there.