From a3755fe0a52cfbadcc92b52ed89a87bdd6b57e76 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Sat, 24 Jan 2026 22:04:36 +1100 Subject: [PATCH] fix: add syntax to recommended_spelling for inv (#12139) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `«term_⁻¹»` to the `recommended_spelling` for `inv`, matching the pattern used by all other operators which include both the function and the syntax in their spelling lists. Reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60recommended_spelling.60.20for.20.60.C2.ABterm_.E2.81.BB.C2.B9.C2.BB.60 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 --- src/Init/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index a1a4efc2c5..b34ed0461f 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -360,7 +360,7 @@ recommended_spelling "smul" for "•" in [HSMul.hSMul, «term_•_»] recommended_spelling "append" for "++" in [HAppend.hAppend, «term_++_»] /-- when used as a unary operator -/ recommended_spelling "neg" for "-" in [Neg.neg, «term-_»] -recommended_spelling "inv" for "⁻¹" in [Inv.inv] +recommended_spelling "inv" for "⁻¹" in [Inv.inv, «term_⁻¹»] recommended_spelling "dvd" for "∣" in [Dvd.dvd, «term_∣_»] recommended_spelling "shiftLeft" for "<<<" in [HShiftLeft.hShiftLeft, «term_<<<_»] recommended_spelling "shiftRight" for ">>>" in [HShiftRight.hShiftRight, «term_>>>_»]