Building
-------------------------
For dependencies see the coq-proba.opam file. The following configuration is
known to work (listed by opam package name and version)

- coq                       8.13.2
- coq-bignums               8.13.0
- coq-coquelicot            3.1.0
- coq-flocq                 3.3.1
- coq-interval              4.3.0
- coq-mathcomp-ssreflect    1.12.0
- coq-stdpp                 1.5.0

We have not tested compilation under other configurations.

You can install dependencies by running `make build-dep`. Proof scripts should
then build by simply typing `make`.


HTML Outline of Files
-------------------------
The file readme.html contains an outline of the paper by section with
links to important lemmas and definitions that are mentioned in the
paper. The CoqDoc html that it links to should be distributed as part
of the supplementary material distribution, but it may have been deleted
if you issued a command line "make clean". To rebuild it, please run
`make html`.

Plaintext Guide to Files
-------------------------

All source files are in the subdirectory theories/, so all the
paths we will quote are with respect to that.

- basic/ -- Some miscellaneous files that do not really belong
  anywhere else: extensions to the ssreflect bigop library, 
  tactics for converting between ssreflect nats and standard library nats,
  etc.

- prob/ -- Basic library of results for discrete probability theory.

- measure/ -- Basic measure theory (lebesgue integral and measure, Fubini's theorem, etc.)

- monad/ -- Definitions of probabilistic choice monads.