leanprover-community / lean4-metaprogramming-book

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

Change variable naming to make it less confusing #111

Open kustosz opened 1 year ago

kustosz commented 1 year ago

In the original text, the choice of m is unfortunate, because m is already bound in the type. While the meaning is clear, it made me to trip and re-parse the paragraph a few times, so I'm proposing this change for ease of reading.