GitLab

Avoid relying on `apply`'s reduction behavior.

See merge request !14

Even if the environment is Cygwin, the compiler might still be the one
from MinGW, so the script no longer relies on uname.

- rounding to nearest, ties to zero
- optimal error for FLT rounding: error_le_opt_FLT
- a few lemmas about rounding to nearest

It is now needed only by the correctness theorems.

This commit also introduces a type class for (prec < emax).