This is a test assignment for the project "Mechanizing Denotational Semantics of Message-Passing Concurrency in the Coq Proof Assistant".
All the theories are located in src/lists.v. You can interpret this file interactively in an IDE. For example, you can use VsCoq.
Otherwise, you can build it using dune:
- First, you have to make sure that Coq is installed. For example, you can install it locally using opam-switch. If you already have a global installation, you can skip this step.
- Then invoke in the command line:
dune build