Commit 2025-08-20 15:48 4cb1b3ce

refactor(Tactic/NormNum): expose the derive API for known expressions directly (#28621) We already exposed these through a janky core method, this now makes them more obviously part of the API, via dot notation. Most of the norm_num changes are just moves out to an auxiliary function. This should make it possible to write ← (← ra.mul rb).add (← rc.mul rd) to derive a term of the form a * b + c * d. This deletes the core methods, but we could instead deprecate them. := by exact q(delta% inferInstance) is from #metaprogramming / tactics > A Qq gotcha @ 💬.