NaNs and infinities are not the hard cases. The hard cases are big exponents and large numbers of decimal digits. In general, it requires arbitrarily large int

NaNs and infinities are not the hard cases. The hard cases are big exponents and large numbers of decimal digits. In general, it requires arbitrarily large integers (OK, OK, up to the maximum size of a double ~2^1023) and long division on said large integers. Denormalized is a pain for sure. Did this recently. https://github.com/titzer/virgil/blob/master/aeneas/src/vst/FpSketch.v3 https://github.com/titzer/virgil/blob/master/aeneas/src/vst/...