From cfb67ee5899da5b98e54744f786957278e46a0ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Feb 2022 09:23:37 -0800 Subject: [PATCH] chore: add `RELEASES.md` It is based on the approach used in rust. --- RELEASES.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 RELEASES.md diff --git a/RELEASES.md b/RELEASES.md new file mode 100644 index 0000000000..d0f0c347f5 --- /dev/null +++ b/RELEASES.md @@ -0,0 +1,17 @@ +v4.0.0-m4 +--------- + +* Support notation `let := | ` in `do` blocks. + +* Remove support for "auto" `pure`. In the [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574), the consensus seemed to be that "auto" `pure` is more confusing than its worth. + +* Remove restriction in `congr` theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid `congr` theorem. +```lean +@[congr] +theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] : + ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ := +``` + +* [Partially applied congruence theorems.](https://github.com/leanprover/lean4/issues/988) + +* Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.