Zulip Chat Archive
Stream: mathlib4
Topic: refine linter
Sky Wilshaw (Aug 20 2023 at 12:10):
Is there a linter that shows uses of refine where exact would suffice?
Eric Wieser (Aug 20 2023 at 12:15):
No, but one would certainly be welcome!
Sky Wilshaw (Aug 20 2023 at 12:19):
Good to know. I don't (yet) know how Lean 4 metaprogramming works, but I'd like to learn in the future.
Last updated: Dec 20 2023 at 11:08 UTC