Functorial implementation of classic algorithms for arithmetic, in OCaml.
https://c-cube.github.io/funarith/
We should have at least:
- simplex for ℚ
- simplex + branch&bound for Z
- solving systems of linear diophantine equations
- omega for Z
- Cooper for Z (quantifier elimination)
$ make
MIT license