| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-01 | Add tests for primitive floats with 'native_compute' | Pierre Roux | |
| Tests are updated to include native computations. | |||
| 2019-11-01 | Add tests for primitive floats with 'vm_compute' | Guillaume Bertholon | |
| Tests are updated to include VM computations and check for double rounding. | |||
| 2019-11-01 | Add tests for primitive floats | Guillaume Bertholon | |
| Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |