leanprover-community / lean4-metaprogramming-book

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

unexpanders should not match on the constant's name #72

Open javra opened 2 years ago

javra commented 2 years ago

but instead use $_ on the match, @sullrich just added a linter for this.