From 231120c1184480da5c466b0c1ceedef4bf841cbc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Mar 2022 20:02:39 -0800 Subject: [PATCH] chore: update `RELEASES.md` --- RELEASES.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index ba27391a5f..44a9e39c4f 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -1,6 +1,17 @@ v4.0.0-m4 (WIP) --------- +* Improve `#eval` command. Now, when it fails to synthesize a `Lean.MetaEval` instance for the result type, it reduces the type and tries again. The following example now works without additional annotations +```lean +def Foo := List Nat + +def test (x : Nat) : Foo := + [x, x+1, x+2] + +#eval test 4 +``` + + * `rw` tactic can now apply auto-generated equation theorems for a given definition. Example: ```lean example (a : Nat) (h : n = 1) : [a].length = n := by