From 8f83999202a89df43ea20f91490637ede7d2f3b2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Jul 2022 06:26:47 -0700 Subject: [PATCH] chore: update release notes --- RELEASES.md | 1 - 1 file changed, 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index fd19eb40fc..7455bbce37 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -6,7 +6,6 @@ Unreleased a panic error message is produced at runtime if `i` is an index out of bounds. `a[i]?` has type `Option α`, and `a[i]?` evaluates to `none` if the index `i` is out of bounds. See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/String.2EgetOp/near/287855425), and issue [#406](https://github.com/leanprover/lean4/issues/406) for additional details. - The notation `a[i, h]` is now syntax sugar for `a[⟨i, h⟩]`. * Update Lake to v3.2.0. See the [v3.2.0 release notes](https://github.com/leanprover/lake/releases/tag/v3.2.0) for detailed changes.