How to notate constructed Nat. numbers with arabic numerals

Stream: lean4

[Jeremy D]

Hi! I'm trying to go through Terry Tao's Analysis I book and implement the chapter introducing natural numbers in lean 4 (while also following the Theorem Proving in Lean 4 online book), and what I'm wanting to do is notate my instance of the natural numbers with the arabic numerals, just like the natural number library in mathlib4 (lean file provided below, apologies for it being a bit messy in places!).

e.g. my zero => 0, (0)++ => 1, ((0)++)++ => 2, ... (Tao denotes the sucessor function with '++')

This is only my guess, but would it involve some inductive 'magic' where I find out how '0123456789' etc are represented (in unicode, ascii?) and line that up with my repeated application of my successor function?

TaoNat.lean

[Sebastian Ullrich]

The typeclass you are looking for is docs4#OfNat. You will need to map Lean's Nat to your encoding.

[Jeremy D]

Thanks for the response! (and apologies for taking a while to post back)

So after digging some more through the aforementioned online book, I also saw that Alex Codes' video here seemed to be following your same advice (https://youtu.be/u_0jWOlDoPw), so I went ahead and followed through with it. It seems everything seems almost good, except the numeral literals themselves seem to remain the same type as the built-in Nat rather than the one I defined unless a function has been applied to them (e.g. #check 0 will give 0 : Nat, but using my successor function (e.g. 0++) will say its type is my custom natural number ℕ).

On another note, my initial worries was that using Lean's built-in natural numbers would somehow also bring with it already proven results and theorems that I'd instead like to implement and prove myself. Would I be correct in saying that in fact, that's not the case, and using Lean's Nat simply means using this particular code here? https://github.com/leanprover/lean4/blob/75252d2b85df8cb9231020a556a70f6d736e7ee5/src/Init/Prelude.lean#L1015-L1021

Also apologies in advance if some of the ways I phrase my question may be slightly off or unclear. Still new to Lean, and happy to clarify or rephrase anything! :+1:

EDIT: Realize after this time that my understanding of this wasn't entirely accurate, and for the reader, I returned back to this question very recently again but as a second discussion in the comment thread of Alex Codes' vid I linked!

(Here's my updated version of that lean file I attached in my first post): TaoNat.lean