Commit 2025-03-18 12:49 4d4e085b

View on Github →

chore: use to_additive for BoundedAdd (#23009) BoundedAdd and BoundedMul results were in separate section of the file that defines them, with very similar proofs. This PR uses to_additive to generate the Add results from the Mul results, and also adds an instance for the Mul case, that was present only for Add.

Estimated changes