From a116a10050916322b603869e5894f78a7aa6049c Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 25 Apr 2023 18:05:48 +0100 Subject: [PATCH] add explanation of the instances --- server/nng/NNG/MyNat/AddCommMonoid.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/server/nng/NNG/MyNat/AddCommMonoid.lean b/server/nng/NNG/MyNat/AddCommMonoid.lean index 27c36c3..6f65e7b 100644 --- a/server/nng/NNG/MyNat/AddCommMonoid.lean +++ b/server/nng/NNG/MyNat/AddCommMonoid.lean @@ -4,6 +4,13 @@ import NNG.MyNat.Addition namespace MyNat -- TODO: Do we need these instances? +-- (kmb) I wanted to introduce these instances as "collectibles" as +-- one went through the "main route" from addition world to power +-- world. If you could make some extra window with those collectibles +-- in, and whenever you have an instance sorry-free it awards you +-- the collectible, that would be great! These things were just +-- precisely the oddball (to my eyes) classes which nat was an instance of, +-- but I think they would make great collectibles. -- instance addSemigroup : AddSemigroup ℕ := -- {