You can use `reverse` in order to reverse the word, by the way, rather than baking the index arithmetic into the `_b` function.
On Sat, May 1, 2021 at 10:01 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > On Saturday, April 24, 2021 at 11:01:09 PM UTC+2 Glauco wrote: > >> 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) >> > > This is really a good idea. By such a definition, we can use the > representations of short words (up to a length of 8, see > http://us2.metamath.org:88/mpeuni/df-s1.html etc.). If the order of the > digits is reversed, as Glauco suggests, i.e. defining > > toNum = ( b e. NN , n e. Word ( 0 ..^ b ) |-> sum_ k e. dom n ( ( n ` k ) > x. ( b ^ ( ( ( # ` n ) - 1 ) - k ) ) ) ) > > then ( 3 toNum <" 2 1 2 1 "> ) would represent the ternary number 2121, > which is ( 2 * 3 ) + 1 ) * 3 ) + 2 ) * 3 ) +1 = 70. The length of the word > n = <" 2 1 2 1 "> is ( # ` n ) = 4, therefore 1 must be subtracted in the > exponent in the definition of toNum. By reversing the order of the > arguments, and using the name _b instead of isNum: > > _b = ( n e. Word ( 0 ..^ b ) , b e. NN |-> sum_ k e. dom n ( ( n ` k ) x. > ( b ^ ( ( ( # ` n ) - 1 ) - k ) ) ) ) > > we would get ( <" 2 1 2 1 "> _b 3 )= ; 70, which seems to be a quite good > and natural representation. > > By the way, with such a definition, we would have ( <" 2 5 7 0 "> _b 10 ) > = ; ; ; 2 5 7 0 > > Alexander > > > > -- > 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/b5d17ac3-7437-47a2-b23c-9ff261fe5178n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b5d17ac3-7437-47a2-b23c-9ff261fe5178n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvXz%2BuBSU%2BXnNR%3D6SA%3DeHDbb7EhkGxgv%2Bp8%3D2tR0QrwxA%40mail.gmail.com.
