Commit 2025-12-17 09:29 c453659c

feat: avoid private irreducible_def using module system (#32861) This PR removes the instances of private irreducible_def, replacing them with a module system based solution, using @[no_expose] to not expose the definition. This helps make proofs shorter, while still not exporting the value of the definition. One case required set_option backward.proofsInPublic false to work. Note that this is turning off the backwards option that is globally set to true. The eventual aim is to have it globally false, so setting it to false locally is not a problem. In order to do this refactor, I locally set

set_option backward.proofsInPublic false
set_option backward.privateInPublic false

so that the module system is happy with the new version.