search

leanprover-community / lean4-metaprogramming-book

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

questions(lean/main/tactics.lean) #79

Closed adomani closed 1 year ago

adomani commented 1 year ago

A few changes that I think may be desirable, but I am not completely sure. Each element of the diff should be interpreted as a question, whether the change is better or worse than the original!

arthurpaulino commented 1 year ago

For these changes it's better to review the didactic structure of the chapter more carefully. I will do it next week. Thank you for the pointers! I'll leave the PR open as a reminder.

arthurpaulino commented 1 year ago

@adomani Yes, your proposals are correct! Can you adjust the PR to fix those please?

adomani commented 1 year ago

Great, done!