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