Just one word of caution about the format statement. It sees numbers that start with a zero as octal numbers, so if you’re asking it to say, turn 0134 into 000134 it will bomb. The solution is simple, though: Just wrap the value with a [string trimleft 0] to first trim all the leading 0’s, if any, before formatting the number with the right number of leading zero’s.
For example:
set xlateOutVals [format “%06s” [string trimleft $xlateInVals 0]]
If you’re sure the values will never have a leading zero, then it’s not necessary. But if they ever might….