You are right that numbers use only base 10 in set.mm, via the definition df-dec $a |- ; A B = ( ( 10 x. A ) + B ) $.
This definition (due to Mario) nicely incorporates decimal number notation into set.mm with a standard definition, without extending the the Metamath language or introducing another variable type (so that we still have wff, setvar, and class as the only types). A slightly awkwardness compared to other languages is that we have to add a ";" prefix for each additional digit, so that 312 base 10 is represented as "; ; ; 3 1 2", but I see that as a small price to pay in order to avoid complicating the metamathematical justification of definitions. Overall, we prefer to have a single standard base for the majority of the work in set.mm in order to avoid duplicate theorems with numbers in different bases (or frequently having to convert between bases inside of proofs). I think it is unlikely that we will add additional bases for the main part of set.mm because of this. When Mario first introduced the idea of df-dec, he started with base 4 because it may have offered certain technical advantages for some of his work, but in the end he (thankfully) settled on base 10, which of course is the most readable to most humans for most purposes. Even though we are unlikely to add other bases for the main part of set.mm, people are free to do whatever they want (up to a point) in their mathboxes. If you want to play around with say base 3, you could introduce a new symbol, say ";3", and a definition like df-ter $a |- ;3 A B = ( ( 3 x. A ) + B ) $. in your mathbox, so that 2121_3 - 212_3 would be represented as ;3 ;3 ;3 2 1 2 1 - ;3 ;3 2 1 2 which even though a little ugly, at least clearly lets the reader know you're working in base 3. If the "3" in ";3" is deemed to be too confusing, another symbol could be used, for example ";;;" (3 semicolons). With more complexity you could have a variable base as an additional argument to the definition, but it would probably be unpleasant to read. Another alternative is the one suggested by Jim Kingdon of summing terms consisting of explicit powers of the base multiplied by the corresponding digit. That would involve no new notation, but of course would involve longer expressions. Norm On Friday, April 23, 2021 at 9:29:37 AM UTC-4 [email protected] wrote: > Hello all! > I'm quite a beginner on metamath. Recently I search on representing > numbers in base other than 10, like in base 3 or base 7 when I formalize > some exercises in number theory. For example, I want to write > 2121_3 - 212_3 (both in base 3). > > I browse through the Th.List on the website and it seems that I didn't > find relevant information. Any hint is welcome! > > Bests Regards > Kunhao > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f46a573c-5cd5-4a84-9ec5-19083fae2b2cn%40googlegroups.com.
