Skip to content

Commit

Permalink
further release notes
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Nov 16, 2023
1 parent be81860 commit 8e5cf64
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ v4.3.0
* By default, `simp` will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by `simp`, and the `decide` tactic may be useful in such cases. The `decide` simp configuration option can be used to locally restore the old `simp` behavior, as in `simp (config := {decide := true})`; this includes using Decidable instances to verify side goals such as numeric inequalities.

* Many bug fixes:
* [Add left/right actions to term tree coercion elaborator and make `^`` a right action](https://github.com/leanprover/lean4/pull/2778)
* [Fix for #2775, don't catch max recursion depth errors](https://github.com/leanprover/lean4/pull/2790)
* [Reduction of `Decidable` instances very slow when using `cases` tactic](https://github.com/leanprover/lean4/issues/2552)
* [`simp` not rewriting in binder](https://github.com/leanprover/lean4/issues/1926)
* [`simp` unfolding `let` even with `zeta := false` option](https://github.com/leanprover/lean4/issues/2669)
Expand Down

0 comments on commit 8e5cf64

Please sign in to comment.