algco

Conats

Defined in conat.v.

Defined in colist.v, application to Sieve of Eratosthenes in sieve.v (extracted to extract/sieve/).

Defined in cotrie.v, regular expression test in RE_test.v (extracted to extract/re/).

Defined in cotree.v, weakest pre-expectation semantics in cocwp.v, equidistribution theorem in equidistribution.v.

Name		Name	Last commit message	Last commit date
Latest commit History 76 Commits
extract		extract
.gitignore		.gitignore
LICENSE		LICENSE
Makefile		Makefile
Q.v		Q.v
R.v		R.v
README.md		README.md
RE_test.v		RE_test.v
_CoqProject		_CoqProject
aCPO.v		aCPO.v
axioms.v		axioms.v
cocwp.v		cocwp.v
cocwp_facts.v		cocwp_facts.v
colist.v		colist.v
conat.v		conat.v
coreal.v		coreal.v
cotree.v		cotree.v
cotrie.v		cotrie.v
cpo.v		cpo.v
eR.v		eR.v
equidistribution.v		equidistribution.v
geometric_series.v		geometric_series.v
inf_primes.v		inf_primes.v
kleene_algebra.v		kleene_algebra.v
misc.v		misc.v
mu.v		mu.v
order.v		order.v
prod.v		prod.v
sieve.v		sieve.v
sieve_relate.v		sieve_relate.v
sum.v		sum.v
tactics.v		tactics.v