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 with let.
  • 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 slow rw.
  • 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).

Estimated changes