mirrors/nixpkgs
1
0
Fork 1
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-11-30 01:20:40 +00:00
Code Issues Wiki Activity
nixpkgs/pkgs/development/coq-modules/domains/darcs_context

810 lines
21 KiB
Plaintext
Raw Normal View History

coqPackages.domains: new expression
2014-10-12 04:01:46 +01:00
Context:
[additional facts about limits on cuts
robdockins@fastmail.fm**20140818025955
Ignore-this: 6f9c952db425df6ae9d2a14139a8a3d1
]
[work on limits
robdockins@fastmail.fm**20140817221707
Ignore-this: 9811e0cd669b48f3beb7a56d47cbe3c3
]
[finish proving that Q field ops commute with injq
robdockins@fastmail.fm**20140817060600
Ignore-this: a1f6c62b39983e6f6f01d28aca5f8534
]
[split up realdom.v and perform associated code motion
robdockins@fastmail.fm**20140817030034
Ignore-this: 24c74cd459d2ab15dcd3d83ba06f7081
]
[recip is canonical and converges
robdockins@fastmail.fm**20140725211947
Ignore-this: c100dbd94114cca9576b2a3f46c9ddc7
]
[improve the proof that 1 is a unit for multiplication
robdockins@fastmail.fm**20140724150124
Ignore-this: c5ec976f8a9858a7ba1f704b4e84d02e
]
[complete proof the interval multiplication converges; other minor stuff
robdockins@fastmail.fm**20140724015132
Ignore-this: bc717baa4c8f9ec31b821c5cfae5b499
]
[further progress in realdom.v
robdockins@fastmail.fm**20140723004023
Ignore-this: f33e18d22ae69c9b6209e28151d18017
]
[unmessify rational_intervals patch
robdockins@fastmail.fm**20140721123718
Ignore-this: 4a125b192a9964a508a1063845e9f160
]
[messy updates to rational_intervals.v
robdockins@fastmail.fm**20140721015810
Ignore-this: 858dac9c55426167c6f397a71ef3fda5
]
[implicit arguments for "fixes"
robdockins@fastmail.fm**20140721015739
Ignore-this: 229ecdd48265fc855319141e399bc522
]
[metadata
robdockins@fastmail.fm**20140714201441
Ignore-this: aa16faaf09c1c404bdc6eaf0d0c39912
]
[further beautification
robdockins@fastmail.fm**20140714200516
Ignore-this: 47d74c51d9fe130a5ac12706b1ddb1d4
]
[start working on the recripricol function
robdockins@fastmail.fm**20140714180055
Ignore-this: c7f93cea17f46daa78a1ea14e86dfcaf
]
[tweaks to the lambda models
robdockins@fastmail.fm**20140714180031
Ignore-this: 219788fe70f42f0f6e60176cab464f19
]
[beauty edits in st_lam*
robdockins@fastmail.fm**20140714180006
Ignore-this: a40aa7ae00ed27595ee04073918bd028
]
[move stuff to rational_intervals.v / define real_mult and prove some properties
robdockins@fastmail.fm**20140712053232
Ignore-this: 398c5c03aac9ff37526d4d7c9e1a82c0
]
[finish correctness proof for interval multiplication
robdockins@fastmail.fm**20140711191547
Ignore-this: c9ab138a0ca43fe0b133b208419bbcc4
]
[break out facts about rational intervals
robdockins@fastmail.fm**20140711012320
Ignore-this: b7fe6e9377629a89b5debe3019ae1aa
]
[updates to ideal completion
robdockins@fastmail.fm**20140707053800
Ignore-this: 90d1efbd0e5833d8c83f0df056d7a74c
]
[a pile of additional properties in realdom.v
robdockins@fastmail.fm**20140707053519
Ignore-this: 7edba1e72a1856f297ef11e698ed989f
]
[some properties of converging prereals
robdockins@fastmail.fm**20140706041401
Ignore-this: 273bfbb245302becd7ff402831827ffb
]
[make realdom compile
robdockins@fastmail.fm**20140630015439
Ignore-this: 8bfc8eaeed4a1596450b0bb9ddef9aaa
]
[renaming
robdockins@fastmail.fm**20140630011639
Ignore-this: a287e083af095790cbf2b48df7a58739
]
[reorganize some code
robdockins@fastmail.fm**20140630011446
Ignore-this: f1375b9e7ad822cb92f0c83d4001eddd
]
[build the retract for realdom
robdockins@fastmail.fm**20140630001245
Ignore-this: 4eb9da621588417d1b7b2fc980c7bf70
]
[fill out lemmas about cPLT
robdockins@fastmail.fm**20140630001140
Ignore-this: add9e45c14621e3d6328684098bf8461
]
[more facts about cPLT
robdockins@fastmail.fm**20140628073731
Ignore-this: 101a131ed114902924a1707eff7ebc70
]
[continuous domains as retracts of bifinite domains
robdockins@fastmail.fm**20140628035522
Ignore-this: 5e7c61d49cf8424412b0d94f5fcb5ee6
]
[start implementing arithmetic operations in RealDom
robdockins@fastmail.fm**20140620003249
Ignore-this: c28479b8a933cba263765bdddb112264
]
[define the domain of rational intervals
robdockins@fastmail.fm**20140619040809
Ignore-this: 6cbe1a9cc690e5a9d77f37ee299154b
this domain is useful for describing the semantics of exact real arithmetic.
]
[show that every effective CUSL is Plotkin
robdockins@fastmail.fm**20140619034433
Ignore-this: d529a4b1d6d698f79572caa805072394
]
[fix notation for octothorpe
robdockins@fastmail.fm**20140614222130
Ignore-this: 3dc815825f11ceaf4f4f53e4668e6382
]
[fix for coq 8.4pl4
robdockins@fastmail.fm**20140614222049
Ignore-this: 9745904845aaf54e5569df982fc93d65
]
[move swelling lemma into finsets
robdockins@fastmail.fm**20140504080535
Ignore-this: ffa560e9aa4e4f8b15a55c1f9b1da72e
]
[documentation improvements and code motion
robdockins@fastmail.fm**20140504070008
Ignore-this: da7847f82403990342732a8ce226315c
]
[replace the old finprod
robdockins@fastmail.fm**20140504005534
Ignore-this: 606cf44422f68d66c8d2d90049e67b93
]
[remove the old finprod
robdockins@fastmail.fm**20140504005137
Ignore-this: 38bd54e16c87d27bbede08496c37bfba
]
[update st_lam_fix to use the new finprod
robdockins@fastmail.fm**20140504003627
Ignore-this: 95d0a66e99ccead89bdfef09a1c8c109
]
[update st_lam to use the new termmodel
robdockins@fastmail.fm**20140503230854
Ignore-this: c3d6b2155674b414c5c2e14b85b13760
]
[new version of finprod with a better term model
robdockins@fastmail.fm**20140503222035
Ignore-this: db63e3a063bdb6f2f579644c7b63bd1b
]
[a few more (hopefully final) lemmas about union
robdockins@fastmail.fm**20140422223924
Ignore-this: 7b95c75abef9b0d45863b5e33d1c5a37
]
[finish proofs about union
robdockins@fastmail.fm**20140422065034
Ignore-this: 2929c3cdb013c028a48022b0293b2f18
]
[powerdomain progress
robdockins@fastmail.fm**20140421064325
Ignore-this: 592f9c6046f05a27897b460edb2efe10
Show that powerdomains are endofunctors on PLT. Further, they are monads with
the 'singleton' and 'join' operations. Also make some progress on the additive
portion of the theory, dealing with emptyset and union.
]
[tweak makefile
robdockins@fastmail.fm**20140420031337
Ignore-this: d5954b26f731bfed3d79cefacab322fb
]
[show that semvalue is the weakest condition allowing beta-reduction of strict functions
robdockins@fastmail.fm**20140420020447
Ignore-this: 16a7ed23f04879f1fb324bdac8a2ffaf
]
[some additional operations relating to the PLT adjunction
robdockins@fastmail.fm**20140420020351
Ignore-this: db8eec6e3f74cce3acb67d2b660b104e
]
[finish building power domain fmap
robdockins@fastmail.fm**20140420020217
Ignore-this: 556e1cb87576de36cb26f8add3a1b163
]
[fix up st_lam.v
robdockins@fastmail.fm**20140329015058
Ignore-this: 1c31d674b759fbd0cc74fb3125579f96
]
[push some proofs into finprod
robdockins@fastmail.fm**20140329000401
Ignore-this: 49070fdd951e49473e60d3cd0ec431c6
]
[documentation and aesthetic changeds
robdockins@fastmail.fm**20140327043141
Ignore-this: be27b24b78ea6af722a307117e59f5b3
]
[finish the st_lam_fix example
robdockins@fastmail.fm**20140322011153
Ignore-this: e702f564b6eab2f8c11ab16bcb62504b
]
[clarafications re: countable choice; remove unfinished example from build order
robdockins@fastmail.fm**20140321212852
Ignore-this: 2a9d5c79c05ba088e1815feab99a5f6c
]
[break the "fixes" operator into a separate file and prove some facts about it
robdockins@fastmail.fm**20140318013247
Ignore-this: 80c506cef0719a974a049a1f5870f676
]
[minor fix to skiy.v
robdockins@fastmail.fm**20140317054057
Ignore-this: ffef6fcaf5fa7f8cea80d2808caf4f4c
]
[add the fixpoint operator; admit proofs
robdockins@fastmail.fm**20140317044648
Ignore-this: 97ca18e980cdf46a9b40c8252badef14
]
[remove the evaluation case for variables
robdockins@fastmail.fm**20140317032932
Ignore-this: e46d634e735e5b21a18518a48777168d
]
[start on STLC with fixpoints -- but without fixpoints for now
robdockins@fastmail.fm**20140317031953
Ignore-this: 3458bc18c73d967bef58418bc73e06cb
]
[add the eliminator for booleans to st_lam; other additional utility lemmas
robdockins@fastmail.fm**20140317031753
Ignore-this: 369dd375755cbd9ae5e3c969f3ef6ec
]
[some minor code motion
robdockins@fastmail.fm**20140228064927
Ignore-this: 804828472ddb0c5fafc72460fce8387b
]
[plug final holes in st_lam and add to build order
robdockins@fastmail.fm**20140228044729
Ignore-this: 3edc7f36bfa97775ba33ffa27c80df59
]
[reduce st_lam.v to facts I believe about fresh variables
robdockins@fastmail.fm**20140228010832
Ignore-this: bde3e73291ddd32337d6fb999e4b1c02
]
[fix breakages
robdockins@fastmail.fm**20140226073930
Ignore-this: 9be54f5255f8ed9d53a79260e9bdf565
]
[more work on lambdas
robdockins@fastmail.fm**20140226043753
Ignore-this: 7f7452670221e2643067a3c7cc180998
]
[use new finprod implementation
robdockins@fastmail.fm**20140226043700
Ignore-this: c9e05df5fcfd31254ed7318fe693490c
]
[remove old finprod
robdockins@fastmail.fm**20140226043642
Ignore-this: 2705703a2c782da21a152fbb27c8a972
]
[rearrange the interfact to finprod
robdockins@fastmail.fm**20140226043541
Ignore-this: c44d7c478948f42b188eb8d06469abbf
]
[fill remaining holes in finprod2
robdockins@fastmail.fm**20140225205242
Ignore-this: 1eeb9b8beef92790c28918292f2a9cf4
]
[rework some stuff dealing with semidecidable predicates
robdockins@fastmail.fm**20140225092149
Ignore-this: 32b5ccb2927e08979ea92b9ef67c40f4
]
[lots of work on alpha-congrunce in lambdas
robdockins@fastmail.fm**20140225035601
Ignore-this: fbbec9dac4cb328ff4e0b25df646e0c7
]
[terminate is universal in PLT
robdockins@fastmail.fm**20140225035538
Ignore-this: abc6cd1a60578c435bf9ca596d8d0922
]
[new attack on nominal finite products
robdockins@fastmail.fm**20140225035516
Ignore-this: 3875e713acc6aa5193696612f3ede76d
]
[push forward a little on lambdas
robdockins@fastmail.fm**20140221095249
Ignore-this: c690a1b03075702e3fd84aac7e268211
]
[update finprod for various changes
robdockins@fastmail.fm**20140221095230
Ignore-this: a6d787930ed356ae2b0a003af1f4d44
]
[better discrete cases lemma
robdockins@fastmail.fm**20140219051301
Ignore-this: f0ec88e8207257e7657ced933cf687e7
]
[start working on simply-typed lambdas
robdockins@fastmail.fm**20140219051238
Ignore-this: 69bea345376ea39cd1addc0849a43077
]
[more messing about with advanced category theory stuff
robdockins@fastmail.fm**20140211095003
Ignore-this: 9cd3c9d961349e8797f109f716c5f678
]
[minor rearrangements and code motion
robdockins@fastmail.fm**20140211041724
Ignore-this: 642ad6f1395fde7ecd81e5a905fd5428
]
[some basic bicategory theory
robdockins@fastmail.fm**20140210083634
Ignore-this: f47a898fa045a397d3ee70e1512b8baa
]
[even more notation futzing
robdockins@fastmail.fm**20140209072416
Ignore-this: d2061652cb3e80f6994f567a9e677b32
]
[additional notational futzing
robdockins@fastmail.fm**20140209043308
Ignore-this: ac42cbbc94df227e6d5e70b96ae65fd3
]
[futz around with notations, various other cleanup activities
robdockins@fastmail.fm**20140209005551
Ignore-this: 3f41a52650aadd956ac490b62e59c1c3
]
[complete adequacy for SKI+Y
robdockins@fastmail.fm**20140206050414
Ignore-this: f730587ac7a42f3e35740976a1439f2e
]
[minor changes in cpo
robdockins@fastmail.fm**20140206014745
Ignore-this: 95244704faf1e6c336d62dc7912f9022
]
[push through most of SKI+Y adequacy
robdockins@fastmail.fm**20140205214805
Ignore-this: dc998ef45f2e919e9373bfa21a5ef8c7
]
[major simplification of the adequacy proof for SKI
robdockins@fastmail.fm**20140205185605
Ignore-this: f1f0dc46274db05f3393038dfe2775e2
]
[push forward on SKI+Y
robdockins@fastmail.fm**20140205044216
Ignore-this: daf255aa940b42c1c68ba947a356370d
]
[continue futzing with the LR statement
robdockins@fastmail.fm**20140203055601
Ignore-this: f5ef9f06d3b1a11d76317b52cec691ab
]
[start pushing on adequacy for SKI+Y
robdockins@fastmail.fm**20140202085948
Ignore-this: 956844809340fad0c13c19e9fa729b5c
]
[mostly finish soundness for SKI+Y
robdockins@fastmail.fm**20140202060633
Ignore-this: 4c75fd9eeefa1d6dad6866662abea0fd
]
[start working on a CCL example
robdockins@fastmail.fm**20140202020748
Ignore-this: 44c5d7854cc19b0f90414c2be6b3df68
]
[make id(A) a parsing-only notation
robdockins@fastmail.fm**20140202020724
Ignore-this: 68f51f754c0b89e2e815da47b901e4b1
]
[the PLT adjunction is strong monodial
robdockins@fastmail.fm**20140202020637
Ignore-this: 7b29b9a6a5e8efa07440c528ec12d7bd
]
[fix my broken version of lfp and fixup proofs
robdockins@fastmail.fm**20140202020615
Ignore-this: 3ac283481318622cbf38378e815a4f09
]
[more work on SKI + Y
robdockins@fastmail.fm**20140202020516
Ignore-this: d1f63e2ef610c6f93d03806c5426cfa5
]
[start work on SKI + Y
robdockins@fastmail.fm**20140201085039
Ignore-this: fb7a405830cf90526cddd8ce37f4da40
]
[doc corrections
robdockins@fastmail.fm**20140130015908
Ignore-this: bca4c04267bfdac8cb202651a0960d92
]
[lots of additional inline documentation
robdockins@fastmail.fm**20140129234834
Ignore-this: ab2c59add5514f44a898de1f0eece98b
]
[powerdomains form continuous functors in EMBED
robdockins@fastmail.fm**20140126234115
Ignore-this: d2ee08902f0bdb52efd7f7ce2c594469
]
[complete the powerdomain constructions; build some operations
robdockins@fastmail.fm**20140125225202
Ignore-this: 9c8f2632df05e84fc3794a338ff8720d
]
[construct the basic powerdomains--still some holes left
robdockins@fastmail.fm**20140125064541
Ignore-this: c3206d2e1e925096b3e9ff49afacef2f
]
[generalize the lfp construction to a generic chain_sup operation
robdockins@fastmail.fm**20140124183103
Ignore-this: 4cc2c1011b9f79365dcb7c76784fbfa6
]
[update makefile
robdockins@fastmail.fm**20140124073734
Ignore-this: a0b7db8383262caa314c21b99e146222
]
[new file for recursive lambda domains
robdockins@fastmail.fm**20140124070023
Ignore-this: 300c02b4da83b6ebd734aa2ccb21cd2d
]
[more lemmas about antistrict homs
robdockins@fastmail.fm**20140124065953
Ignore-this: 483c7b350dc3cab59c8ff50e1ac73b8c
]
[fix breakage related to implicit arguments
robdockins@fastmail.fm**20140124065805
Ignore-this: 561693d3280851299c6a49a2a34546b3
]
[notation tweaks in cpo.v
robdockins@fastmail.fm**20140124053800
Ignore-this: 83e92d8c14568448074a940ceafbe2c9
]
[add if/then/else to the SKI system
robdockins@fastmail.fm**20140124023630
Ignore-this: 37a9737932a05393a6338380226ca346
]
[case analysis for finite types
robdockins@fastmail.fm**20140124012505
Ignore-this: 6ec1076b2a74f5832501a105a28a6dba
]
[finish adequacy proof for SKI
robdockins@fastmail.fm**20140123211322
Ignore-this: 1fe3e626e33431c27e2aa186b3bf91d2
]
[additional lemmas about domains
robdockins@fastmail.fm**20140123090037
Ignore-this: fcad2dd816f805b8b5e7d1be3df60db8
]
[most of a proof of adequacy for SKI
robdockins@fastmail.fm**20140123085839
Ignore-this: d1595c02a6387297018e7f316a3e751
]
[more work on finite products
robdockins@fastmail.fm**20140121061158
Ignore-this: c2f8212e041478104dd4c81c225b42d5
]
[begin work on a more flexible "finprod" domain
robdockins@fastmail.fm**20140119021653
Ignore-this: 249718a2c31964733171b21c84d2effb
]
[mess with implicit arguments in categories.v
robdockins@fastmail.fm**20140113041450
Ignore-this: 314cad9207f706e949bd686aaa5c5e1b
]
[products for CPO, uniformity of lfp
robdockins@fastmail.fm**20140113041421
Ignore-this: e533abe995e634c732a35e71d66ddb6a
]
[define the LFP in pointed CPOs, prove the Scott induction principle
robdockins@fastmail.fm**20140112231843
Ignore-this: 2014174b1c6914bef376d614f34d073f
]
[build the forgetful functor from EMBED to PLT
robdockins@fastmail.fm**20140110014909
Ignore-this: 1dacbfc0383e48f4ab35fe0a5fd11cec
]
[notation changes, prove sum_cases and curry preserve order and equality
robdockins@fastmail.fm**20140110014820
Ignore-this: d1c6a1d0346a9eba14f3529ac30b5e2f
]
[prove addl facts about pairs, tweak implicit arguments
robdockins@fastmail.fm**20140110010319
Ignore-this: 9f0af8abc268b2b22d8b5450d6a4136
]
[make 'ob' a coercion
robdockins@fastmail.fm**20140110010204
Ignore-this: 467c0b0a8b086a7f44bf98875a4380d6
]
[copyright notices
robdockins@fastmail.fm**20140106232333
Ignore-this: f59bafa0ec99e259bd9b4319f2cdbc67
]
[add ord_dec coercion
robdockins@fastmail.fm**20140104052750
Ignore-this: 4ed1cacfd27979f0fe518862be5ac27c
]
[define the model for CBV lambda calculus
robdockins@fastmail.fm**20140104050626
Ignore-this: 88ca796d4697bfebb044d3fae27d6129
]
[proof a fixpoint lemma for unpointed domains
robdockins@fastmail.fm**20140103231818
Ignore-this: 4939eb02d09b6a4eecf145c887c64393
]
[prove that the adjoint functors between PLT and PPLT extend to continuous functors in EMBED
robdockins@fastmail.fm**20140103000915
Ignore-this: 54da0101f581731ebe512ed514e0603e
]
[notation changes for PLT
robdockins@fastmail.fm**20140102234446
Ignore-this: ad1f82f22d1bf0e057f11c3508a81716
]
[move embeddings into their own file; pull TPLT and PPLT into profinite.v
robdockins@fastmail.fm**20140102234424
Ignore-this: 3704996af47ae32415ba3e539d67cf5c
]
[Show that PLT is cocartesian; rearrange proof that EMBED(true) is terminated
robdockins@fastmail.fm**20140102213805
Ignore-this: 3470df6910e7a3e4bda478c0c6ecea62
]
[remove unnecessary "inh" hypothesis in the definition of Plotkin order; fixup the fallout
robdockins@fastmail.fm**20140102213646
Ignore-this: b6a5ad59296f938b377d71852120d48b
]
[move proofs that empty and unit preorders are effective plotkin
robdockins@fastmail.fm**20140102205530
Ignore-this: 7324843510fd938d356aa82003c9ec68
]
[make epi/mono/iso morphisms into categories
robdockins@fastmail.fm**20131228082442
Ignore-this: ee75a2b6eb1f3d6fa47f17d6734e5015
]
[define the cocartesian and distributive categories
robdockins@fastmail.fm**20131226001612
Ignore-this: 11e9d8a88bef42bcb800b31d85d28d16
]
[remove uses of maximally implict arguments
robdockins@fastmail.fm**20131226001536
Ignore-this: c0d93a5398aea58cbcc4fbbca3b59b17
]
[fixpoints and binary sums for NOMINAL
robdockins@fastmail.fm**20131121092931
Ignore-this: 8a660dfe2ab16a8208ae559dcf2b7ed0
]
[modify bilimit.v to use the general construction from cont_functors.v
robdockins@fastmail.fm**20131120075848
Ignore-this: 17ea36107ade1646eab5c99aec3561a9
]
[generic fixpoint construction for categories with initial objects and directed colimits
robdockins@fastmail.fm**20131119092522
Ignore-this: 25674dff855a1cecdb4ee919f8bf3a5d
]
[remove some irritating unit parameters, fix doc typos
robdockins@fastmail.fm**20131118093204
Ignore-this: 38342d58567d8a13471620d5b7c2b7d4
]
[improvements to categories; complete some constructions in nominal
robdockins@fastmail.fm**20131118085737
Ignore-this: e58cb49a01d0210dabdb021250910adb
]
[build fixes
robdockins@fastmail.fm**20131113004305
Ignore-this: 5abffcd1d6b44f816749c5e0cfd5b6e9
]
[Documentation additions
robdockins@fastmail.fm**20131113004254
Ignore-this: 79a913d3a8652866f3fdc64891f6304d
]
[lots of inline documentation additions
robdockins@fastmail.fm**20131112192736
Ignore-this: 6aa38112c10ceed3bf43e35dbda98312
]
[update makefiles
robdockins@fastmail.fm**20131112192706
Ignore-this: d834beaa532cdf994cfa0a0b5a562e4f
]
[continuous functors for binary sum and products
robdockins@fastmail.fm**20131112192605
Ignore-this: 61520e6e315df909465a02f854816366
]
[add the category of nominal types
robdockins@fastmail.fm**20131112192520
Ignore-this: f0351c5eb0bdacdfe192a6863d9c0bc6
]
[split the proof that expF is a continuous functor into a separate file; rearrange some defintions
robdockins@fastmail.fm**20130924013328
Ignore-this: 4eacee37bb6474d1bdfffe416b98b4c1
]
[rearrange definitions of continuous functors. Prove enough plumbing to build the model: D = D->D
robdockins@fastmail.fm**20130924002837
Ignore-this: a66f9e8833601e244048b70e8bfaab96
]
[show that the function space is a continuous functor; other junk
robdockins@fastmail.fm**20130923060521
Ignore-this: d8f406450688c633ebc1fe1eb0343c91
]
[some name changes, other cosmetic fixes
robdockins@fastmail.fm**20130909043234
Ignore-this: cdd24d1c96a34fb3573c1806153df9fb
]
[additional cosmetic changes and rearrangements
robdockins@fastmail.fm**20130909020137
Ignore-this: 77d28bc9452f6c93915194033118dab7
]
[reorganize profinite code
robdockins@fastmail.fm**20130909011437
Ignore-this: 8511bf92ca6998ff8c69d5537624bdb8
]
[cosmetic changes
robdockins@fastmail.fm**20130908183909
Ignore-this: e19039701e58fd26ca4eab79d7b49d14
]
[complete the bilimit construction, show how to take fixpoints of continuous functors
robdockins@fastmail.fm**20130908175228
Ignore-this: 82feab8fdc0c944f13d91605c6a8e571
]
[find a MUCH easier path to a bilimit construction
robdockins@fastmail.fm**20130907012151
Ignore-this: fcc72ad140b045ef37e4b03ad38a8fb0
]
[lots of progress, mostly on defining bilimits
robdockins@fastmail.fm**20130905204959
Ignore-this: abf4bcf03a49fa009f9fb2200ee3abf2
]
[start working on the theory of finite preorders, which form a basis for plokin orders
robdockins@fastmail.fm**20130812054451
Ignore-this: 5be36257a8fdf486bcc31f587d93c457
]
[parameterize plotkin orders, build category PPLT
robdockins@fastmail.fm**20130811063623
Ignore-this: 3f273841bc72098acee0fd618627dbd5
]
[complete the details showing PLT is cartesian closed
robdockins@fastmail.fm**20130809230336
Ignore-this: 13fd1b5a8172dd263cf655421f7584f7
]
[add files missed in the first import
robdockins@fastmail.fm**20130809080742
Ignore-this: 6b59cce866a486d70559f7c80fe99053
]
[initial import of development
robdockins@fastmail.fm**20130809080409
Ignore-this: 44cb5a0df2f1643d289f07dcd4227cbf
First major steps toward a fully effective and usable formalized
domain theory. We formalize the plotkin preorders and show that
they form a cartesian closed category.
]
Copy permalink