feat: safe exponentiation - Adds configuration option `exponentiation.threshold` - An expression `b^n` where `b` and `n` are literals is not reduced by `whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`. Motivation: prevents system from becoming irresponsive. TODO: improve support in the kernel. It is using a hard-coded limit for now.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).