max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: use notMem instead of not_mem in recommended_spelling (#8496)

Browse source 
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)
This commit is contained in:
Sebastien Gouezel 2025-06-02 08:46:36 +02:00 • committed by GitHub
parent 0339cd2836
commit 3516143aed
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Notation.lean
View file

@ -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