REQUIREMENTS

## For simple typechecking

- around 5GiB free space on disk
- docker (has been tested with v27.3.1, should work with older versions)

To simply typecheck the code with the docker image, only a working docker
daemon is required. Install it from your distribution's package manager, or see
https://docs.docker.com/desktop/. This has only been tested on linux/amd64, but
should work out of the box on windows as well as macos. In case you are on a
non amd64 plateform (eg apple silicon or some other aarch64), the flag
`--plateform linux/amd64` needs to be added to all the docker commands.

## For local installation

- dune
- coq 8.17
- coq-equations 1.3+8.17
- coq-coinduction 1.6

The recommended way to install the requirements is through the coq-released
opam repository. The steps for doing so are detailed at the end of the README
file.