An ACL2 string with the amount. In practice, the amount should
match either unsigned_number or fixed_point_number,
e.g., "3" or "45.617". We don't try to process
this further because (1) we don't expect it to matter for much,
and (2) ACL2 doesn't really support fixed point numbers.