lean4-metaprogramming-book
lean4-metaprogramming-book
copied to clipboard
Published
20 hours ago
•
leanprover-community
Reame
Issues
unexpanders should not match on the constant's name
Open
javra
opened this issue 1 year ago
• 0 comments
but instead use
$_
on the match, @sullrich just added a
linter
for this.
Jul 28 '22 14:07
javra