chore: the previous commit exposed an issue with `simp` `simp` was previously swallowing runtime exceptions and masking an issue with this example. `runT` is defined by well-founded recursion, but reducing the ground term `runT x` takes a long time when `decide := true`. Remark PR #2722 changes the `decide` default value to `false`. When `decide := true`, we should probably have better diagnostics / error messages for this kind of situation.
This is the repository for Lean 4.
We provide nightly releases and have just begun regular stable point releases.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.