From 8ce98e62ac82379caaa4e76243e8f4ac3fccf366 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 22 Mar 2024 11:25:44 -0700 Subject: [PATCH] fix: typos in release notes (#3742) --- RELEASES.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 032e64665d..0a8d627fde 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -21,7 +21,7 @@ v4.8.0 (development in progress) * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems). -* New command `derive_functinal_induction`: +* New command `derive_functional_induction`: Derived from the definition of a (possibly mutually) recursive function defined by well-founded recursion, a **functional induction principle** is @@ -42,7 +42,7 @@ v4.8.0 (development in progress) ``` * The termination checker now recognizes more recursion patterns without an - explicit `terminatin_by`. In particular the idiom of counting up to an upper + explicit `termination_by`. In particular the idiom of counting up to an upper bound, as in ``` def Array.sum (arr : Array Nat) (i acc : Nat) : Nat := @@ -88,11 +88,9 @@ fact.def : -/ ``` -v4.7.0 -Breaking changes: - * The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`. +* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`. -v4.7.0 (development in progress) +v4.7.0 --------- * `simp` and `rw` now use instance arguments found by unification,