A Coq library for domain theory (http://rwd.rdockins.name/domains/)

additional facts about limits on cuts

robdockinsMon Aug 18 02:59:55 UTC 2014

work on limits

robdockinsSun Aug 17 22:17:07 UTC 2014

finish proving that Q field ops commute with injq

robdockinsSun Aug 17 06:06:00 UTC 2014

split up realdom.v and perform associated code motion

robdockinsSun Aug 17 03:00:34 UTC 2014

recip is canonical and converges

robdockinsFri Jul 25 21:19:47 UTC 2014

improve the proof that 1 is a unit for multiplication

robdockinsThu Jul 24 15:01:24 UTC 2014

complete proof the interval multiplication converges; other minor stuff

robdockinsThu Jul 24 01:51:32 UTC 2014

further progress in realdom.v

robdockinsWed Jul 23 00:40:23 UTC 2014

unmessify rational_intervals patch

robdockinsMon Jul 21 12:37:18 UTC 2014

messy updates to rational_intervals.v

robdockinsMon Jul 21 01:58:10 UTC 2014

implicit arguments for "fixes"

robdockinsMon Jul 21 01:57:39 UTC 2014

metadata

robdockinsMon Jul 14 20:14:41 UTC 2014

further beautification

robdockinsMon Jul 14 20:05:16 UTC 2014

start working on the recripricol function

robdockinsMon Jul 14 18:00:55 UTC 2014

tweaks to the lambda models

robdockinsMon Jul 14 18:00:31 UTC 2014

beauty edits in st_lam*

robdockinsMon Jul 14 18:00:06 UTC 2014

move stuff to rational_intervals.v / define real_mult and prove some properties

robdockinsSat Jul 12 05:32:32 UTC 2014

finish correctness proof for interval multiplication

robdockinsFri Jul 11 19:15:47 UTC 2014

break out facts about rational intervals

robdockinsFri Jul 11 01:23:20 UTC 2014

updates to ideal completion

robdockinsMon Jul 7 05:38:00 UTC 2014

a pile of additional properties in realdom.v

robdockinsMon Jul 7 05:35:19 UTC 2014

some properties of converging prereals

robdockinsSun Jul 6 04:14:01 UTC 2014

make realdom compile

robdockinsMon Jun 30 01:54:39 UTC 2014

renaming

robdockinsMon Jun 30 01:16:39 UTC 2014

reorganize some code

robdockinsMon Jun 30 01:14:46 UTC 2014

build the retract for realdom

robdockinsMon Jun 30 00:12:45 UTC 2014

fill out lemmas about cPLT

robdockinsMon Jun 30 00:11:40 UTC 2014

more facts about cPLT

robdockinsSat Jun 28 07:37:31 UTC 2014

continuous domains as retracts of bifinite domains

robdockinsSat Jun 28 03:55:22 UTC 2014

start implementing arithmetic operations in RealDom

robdockinsFri Jun 20 00:32:49 UTC 2014