A Coq library for domain theory (http://rwd.rdockins.name/domains/)
root
- LICENSE
- Make
- Makefile
- README
- algebraic.v
- approx_rels.v
- atoms.v
- basics.v
- bicategories.v
- bilimit.v
- categories.v
- ccl.v
- cont_adj.v
- cont_functors.v
- cont_profinite.v
- cpo.v
- cusl.v
- directed.v
- discrete.v
- effective.v
- embed.v
- enriched.v
- esets.v
- exp_functor.v
- finord.v
- finprod.v
- finsets.v
- fixes.v
- flat.v
- ideal.v
- joinable.v
- lam_models.v
- mk_tar.sh
- nominal.v
- notations.v
- pairing.v
- permutations.v
- plotkin.v
- powerdom.v
- preord.v
- profinite.v
- profinite_adj.v
- rational_intervals.v
- realcuts.v
- realdom.v
- reallimit.v
- realops.v
- sets.v
- ski.v
- skiy.v
- st_lam.v
- st_lam_fix.v
- strict_utils.v
- sumprod_functor.v
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/