I've never played with Words in set.mm, but it looks like you could define something like
toNum = ( b e. NN , n e. Word ( 0 ..^ b ) |-> sum_ k e. dom n ( ( n ` k ) x. ( b ^ k ) ) ) where b is your base and n is your representation in base b (please, note that ( n ` 0 ) would be your least significant digit, you should change the ( n ` k ) expression if you want it to be your most significant digit) Glauco Il giorno venerdì 23 aprile 2021 alle 15:29:37 UTC+2 [email protected] ha scritto: > 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/e0c4cb86-4369-4bea-afa7-08d20b757422n%40googlegroups.com.
