From 3516143aed6de08ee44de2beb8e26fab22033831 Mon Sep 17 00:00:00 2001 From: Sebastien Gouezel Date: Mon, 2 Jun 2025 08:46:36 +0200 Subject: [PATCH] doc: use `notMem` instead of `not_mem` in `recommended_spelling` (#8496) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes the recommended spelling from `not_mem` to `notMem`, to reflect the decision that has been made in mathlib. It does *not* change the name of any core lemma. See Zulip discussion at [#mathlib4 > Naming: nmem vs not_mem @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.3A.20nmem.20vs.20not_mem/near/520315224) --- 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 0d60860ff0..f9247cd26e 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -432,7 +432,7 @@ recommended_spelling "not" for "!" in [not, «term!_»] notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b) recommended_spelling "mem" for "∈" in [Membership.mem, «term_∈_»] -recommended_spelling "not_mem" for "∉" in [«term_∉_»] +recommended_spelling "notMem" for "∉" in [«term_∉_»] @[inherit_doc] infixr:67 " :: " => List.cons @[inherit_doc] infixr:100 " <$> " => Functor.map