; simply return an integer
#x123456789