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.15.2 - coq-bignums 8.15.0 - coq-coquelicot 3.2.0 - coq-flocq 4.1.0 - coq-interval 4.5.2 - coq-mathcomp-ssreflect 1.15.0 - coq-stdpp 1.8.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.