Commit 2023-07-09 00:37 2d62a695

fix: norm_num extension for Nat.pow (#5740) Alternative to leanprover/lean4#2310. The original implementation of the pow extension would force a Nat.pow application by defeq, but this should only be done for kernel-approved definitions and Nat.pow is not one of them. Rather than adding more things to the kernel, we can implement an efficient pow implementation by binary recursion, using the clauses:

• a ^ (2*b) = a^b * a^b
• a ^ (2*b + 1) = a^b * a^b * a