Performance improvements
Some points where I think performance can still be improved:
-
AsSolveGoal
TC search is slow. this is now improved -
Definitions like
IntroduceHyp
are not sealed off. Seems to have no effect on performance though: with sealed definitions vs without sealed definitions. - Stripping
□
of persistent hypothesis on introduction is slow? -
Dedicated typeclass for
∀.. (tt: TT), ...
Has no effect on performance: with dedicated typeclass vs without dedicated typeclass. But TC search debug output is more readable. Continued: in the end there was a (small) performance improvement, just a bit later: this vs this. But quite possibly this was due torewrite /term
being slower thanunfold term
.