There is yet another possibility, which is the one I like best: #x1234e57 means (* #x1234 (expt #x10 #x57))