OUVerT

Ohio University Verification Toolsuite

REQUIREMENTS

coq 8.9.0 mathcomp algebra 1.7.0 mathcomp fingroup 1.7.0 mathcomp ssreflect 1.7.0

To build OUVerT, clone it and do:

make

make install

The latter command installs the OUVerT files in your local .opam directory.

To use OUVerT files in another development, simply import them with OUVerT.filename, as in:

Require Import OUVerT.dyadic.

Following are the primary files in the development:

Name		Name	Last commit message	Last commit date
Latest commit History 139 Commits
Makefile		Makefile
README.md		README.md
_CoqProject		_CoqProject
axioms.v		axioms.v
banach.v		banach.v
bigops.v		bigops.v
chernoff.v		chernoff.v
compile.v		compile.v
dist.v		dist.v
dyadic.v		dyadic.v
enumerables.v		enumerables.v
expfacts.v		expfacts.v
extrema.v		extrema.v
generalized_bigops.v		generalized_bigops.v
gibbs_bernoulli.v		gibbs_bernoulli.v
learning.v		learning.v
listlemmas.v		listlemmas.v
maplemmas.v		maplemmas.v
numerics.v		numerics.v
orderedtypes.v		orderedtypes.v
strings.v		strings.v
vector.v		vector.v