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

robdockins / domains Public

Notifications You must be signed in to change notification settings
Fork 2
Star 6

A formal development of constructive domain theory in Coq

Notifications

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/