GitHub - robdockins/domains: A formal development of constructive domain theory in Coq

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 181 Commits
.gitignore		.gitignore
LICENSE		LICENSE
Makefile		Makefile
README		README
_CoqProject		_CoqProject
algebraic.v		algebraic.v
approx_rels.v		approx_rels.v
atoms.v		atoms.v
basics.v		basics.v
bicategories.v		bicategories.v
bilimit.v		bilimit.v
categories.v		categories.v
ccl.v		ccl.v
cont_adj.v		cont_adj.v
cont_functors.v		cont_functors.v
cont_profinite.v		cont_profinite.v
cpo.v		cpo.v
cusl.v		cusl.v
directed.v		directed.v
discrete.v		discrete.v
effective.v		effective.v
embed.v		embed.v
enriched.v		enriched.v
esets.v		esets.v
exp_functor.v		exp_functor.v
finord.v		finord.v
finprod.v		finprod.v
finsets.v		finsets.v
fixes.v		fixes.v
flat.v		flat.v
ideal.v		ideal.v
joinable.v		joinable.v
lam_models.v		lam_models.v
mk_tar.sh		mk_tar.sh
nominal.v		nominal.v
notations.v		notations.v
pairing.v		pairing.v
permutations.v		permutations.v
plotkin.v		plotkin.v
powerdom.v		powerdom.v
preord.v		preord.v
profinite.v		profinite.v
profinite_adj.v		profinite_adj.v
rational_intervals.v		rational_intervals.v
realcuts.v		realcuts.v
realdom.v		realdom.v
reallimit.v		reallimit.v
realops.v		realops.v
sets.v		sets.v
ski.v		ski.v
skiy.v		skiy.v
st_lam.v		st_lam.v
st_lam_fix.v		st_lam_fix.v
strict_utils.v		strict_utils.v
sumprod_functor.v		sumprod_functor.v

Repository files navigation

Copyright (c) 2014, Robert Dockins

This directory contains files that implement a library for domain theory in Coq.
The library is known to compile with Coq version 8.4 and 8.4pl4.

Further information about this library and updates may be found at:

    http://rwd.rdockins.name/domains/