Commit 2024-10-15 22:29 341d9cfc

feat: use @[csimp] to use exponentiation by repeated squaring at runtime (#8885) Using a @[csimp] attribute we can replace npowRec at runtime with an algorithm that uses repeated squaring, without affecting the definitional properties of npowRec. The prototypical application is that

#eval (3 : ZMod 49999)^49998

used to stack overflow, but now runs fine. (This is an output of the "Formalization and Computer Algebra Systems" group at https://aimath.org/workshops/upcoming/cyberinfrastructure/.)