lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
Change variable naming to make it less confusing
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.