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

Change variable naming to make it less confusing

Open kustosz opened this issue 2 years ago • 0 comments

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.

kustosz avatar Jul 19 '23 21:07 kustosz