Commit 2025-02-02 13:52 794c8dd9
View on Github →perf: fix some slow declarations (#21323) This PR fixes some slow declarations, by
- changing the proof slightly so that unification is happier
- giving more arguments in a
rw
theorem - replacing a slow
set
withlet
. - explicitly supplying an autoparam proof, or adding the result to the context to help the autoparam.
- fixing a type so that a slow
erw
can become a less slowrw
. - replacing
‹Ring R›
with(‹Ring R›:)
, which forces the expression to be fully elaborated immediately, instead of temporarily turning into a synthetic metavariable. - reordering the instances in a spread construction of an instance (so that the ancestor that is represented as a subobject field comes first). See also #21030 for another example of this. To find most of these, I took a look at the declarations that use at least 100000 heartbeats (i.e. at least half of the default maximum).