mathlib
cf231995 - chore(number_theory/lucas_lehmer): remove `has_to_pexpr` instances (#14905)

Commit
3 years ago
chore(number_theory/lucas_lehmer): remove `has_to_pexpr` instances (#14905) These instances are sort of out-of-place, and aren't really needed anyway. We already use the more verbose ``%%`(n)`` notation elsewhere in mathlib, which as an operation makes more conceptual sense. Until #14901 these two instances were just special cases of `has_reflect.has_to_pexpr`. While unlike that instance these two instances are not diamond-forming, they're unecessary special cases that make antiquoting harder to understand.
Author
Parents
Loading