Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: DiscrTree: index the domain of
∀
It bothered me that inferring instances of the shape `Decidable (∀ (x : Fin _), _)` will go linearly through all instances of that shape, even those that are about `∀ (x : Nat), …`. And that `Decidable (∃ (x : Fin _), _)` gets better indexing than `Decidable (∀ (x : Fin _), _)`. Judging from code comments, the discr tree used to index arrow types with two arguments (domain and body), and that led to bugs due to the dependency, so the arguments were removed. But it seems that indexing the domain is completely simple and innocent. So let’s see what happens… Mostly only insignificant perf improvements, unfortunately (~Mathlib.Data.Matroid.IndepAxioms — instructions -11.4B, overall build instructions -0.097 %): http://speed.lean-fro.org/mathlib4/compare/dd333cc1-fa26-42f2-96c6-b0e66047d0b6/to/6875ff8f-a17c-431d-8b8b-2f00799be794 This is just a small baby step compared to the more invasive improvements done in the [`RefinedDiscrTree` by J. W. Gerbscheid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp/RefinedDiscrTree.html) in mathlib.
- Loading branch information