Commit 2024-04-29 06:58 4e22ca74

feat: add an OfScientific instance for NNRat and NNReal (#12485) The existing RatCast.toOfScientific instance has to be removed since it forms a non-defeq diamond (there is nothing enforcing that nnratCast and ratCast are defeq). The norm_num extension also needs some fixes, though the old design didn't make much sense anyway, as it synthesize the instances separately, thus losing important defeqs.