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

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.

javra avatar Jul 28 '22 14:07 javra