Commit 2024-02-10 01:29 d43db9f5

chore(Tactic/CancelDenoms/Core): Qq-ify (#9422) This means all the unification is done at compile-time rather than runtime. To make the type of the proof expressible with Qq, we have to construct the numeric literal up front. I can't actually measure a meaningful performance difference in the tactic now, but this spelling is more strongly-typed, and thus the semantics are clearer.