32%R
     : R
(-31)%R
     : R
1.5%R
     : R
1.5e1%R
     : R
eq_refl : 1.02 = 102e-2
     : 1.02 = 102e-2
1.02e1
     : R
102e-1
     : R
1.02e3
     : R
102e1
     : R
1.02e2
     : R
102
     : R
10.2e-1
     : R
1.02
     : R
eq_refl : -0.0001 = -1e-4
     : -0.0001 = -1e-4
eq_refl : -0.50 = -50e-2
     : -0.50 = -50e-2
eq_refl : -26 = -26
     : -26 = -26
eq_refl : 0xb.2c%xR = 0xb2cp-8%xR
     : 0xb.2c%xR = 0xb2cp-8%xR
eq_refl : -6882 = -6882
     : -6882 = -6882
0xb.2cp2%xR
     : R
0xb2cp-6%xR
     : R
0xb.2cp8%xR
     : R
2860
     : R
(-0xb.2cp-2)%xR
     : R
- 0xb2cp-10%xR
     : R
0
     : R
0
     : R
42
     : R
42
     : R
1.23
     : R
0x1.23%xR
     : R
0.0012
     : R
42e3
     : R
42e-3
     : R
0x0
     : R
0x0
     : R
0x2a
     : R
0x2a
     : R
1.23%R
     : R
0x1.23
     : R
0x0.0012
     : R
0x2ap3
     : R
0x2ap-3
     : R