Pretty-printer dot-notation with `Nat.Prime`

Stream: new members

[Snir Broshi]

Why does the pretty-printer not use dot-notation for Nat.Prime?
It converts n.Prime into Nat.Prime n, but other definitions seem fine with dot notation:

import Mathlib

/--
error: unsolved goals
n : ℕ
⊢ Nat.Prime n
-/
#guard_msgs in
theorem foo1 (n : ℕ) : n.Prime := by {}

def Nat.Prime' := Nat.Prime
/--
error: unsolved goals
n : ℕ
⊢ n.Prime'
-/
#guard_msgs in
theorem foo2 (n : ℕ) : n.Prime' := by {}

/--
error: unsolved goals
n : ℕ
⊢ n.Abundant
-/
#guard_msgs in
theorem foo3 (n : ℕ) : n.Abundant := by {}

Setting pp.fieldNotation and pp.fieldNotation.generalized doesn't help.
This only happens on live-lean, in my local Mathlib it does use dot-notation.

[Kyle Miller]

The @[pp_nodot] here is the cause: https://github.com/leanprover-community/mathlib4/blob/ae275c9caf8c85839613ec54cc150ea563af7908/Mathlib/Data/Nat/Prime/Defs.lean#L41