mathlib
5cba21d8 - chore(*): swap order of [fintype A] [decidable_eq A] (#3705)

Commit
5 years ago
chore(*): swap order of [fintype A] [decidable_eq A] (#3705) @fpvandoorn suggested in #3603 swapping the order of some `[fintype A] [decidable_eq A]` arguments to solve a linter problem with slow typeclass lookup. The reasoning is that Lean solves typeclass search problems from right to left, and * it's "less likely" that a type is a `fintype` than it has `decidable_eq`, so we can fail earlier if `fintype` comes second * typeclass search for `[decidable_eq]` can already be slow, so it's better to avoid it. This PR applies this suggestion across the library. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading