float_parts_1e30(1.0e+30, 0.0).
float_parts_neg1e30(-1.0e+30, 0.0).
float_parts_1e300(1.0e+300, 0.0).
float_parts_zero(0.0, 0.0).