Mentions légales du service

Skip to content

Add "remove_unused:dependency" to int.ComputerDivision

David Ewert requested to merge remove_unused_dep_comp_div into master

Adds the "remove_unused:dependency" meta to the axioms and lemmas in int.ComputerDivision. This is especially helpful since most of the mach.int modules use int.ComputerDivision so currently using these modules results in instantiating all of ComputerDivision props (as well as the Abs props and CompatOrderMult) even when none of them are needed.

Merge request reports