Skip to content
/ domains Public
forked from robdockins/domains

A formal development of constructive domain theory in Coq

License

BSD-3-Clause license
0 stars 2 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

hengchu/domains

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

179 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:https://rwd.rdockins.name/domains/

About

A formal development of constructive domain theory in Coq

Resources

Readme

License

BSD-3-Clause license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Coq 99.5%
  • Other 0.5%