From e55da341a671ee4a4debcffe77efbff2c3d3316f Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 28 Sep 2025 09:40:24 +0100
Subject: [PATCH] fix: remove dot notation on MyNat.succ (#119)

---
 Game/MyNat/Definition.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
index 2270acb..e654771 100644
--- a/Game/MyNat/Definition.lean
+++ b/Game/MyNat/Definition.lean
@@ -6,6 +6,8 @@ inductive MyNat where
 | succ : MyNat → MyNat
 -- deriving BEq, DecidableEq, Inhabited
 
+attribute [pp_nodot] MyNat.succ
+
 @[inherit_doc]
 notation (name := MyNatNotation) (priority := 1000000) "ℕ" => MyNat
 -- Note: as long as we do not import `Mathlib.Init.Data.Nat.Notation` this is fine.