From af1e670270eabd9a0c4c42899b961444bc7ebc60 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Jul 2022 15:46:54 -0700 Subject: [PATCH] chore: fix typo --- RELEASES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index 692a57590e..a87995132a 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -19,7 +19,7 @@ Unreleased class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where getElem (xs : Cont) (i : Idx) (h : Dom xs i) : Elem ``` - The notation `a[i]` is not defined as follows + The notation `a[i]` is now defined as follows ```lean macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic)) ```