Starting with inventory: 0000026699-d6c10fbb70f9a32405ef1d50774630189ab2af63f406f1453b2755e8b6b2ebf6 [TAG 0.6 Nils Anders Danielsson **20111227194340 Ignore-this: 2a7b42ee6c56ee2a9bfb81a1ae05ad5f ] hash: 0000018616-525c0dfcd01bec86d54aa63b7df4fdf36b73d715f8d0f1e10fe3a33eaf485d0d [Removed release-specific information. Nils Anders Danielsson **20111227195401 Ignore-this: ec5d8cd6e014686e902bcbc168466316 ] hash: 0000000612-5ccd539b418a58322390dc7b3ce1e3c53452dfe2c7db62e3725cb1da0a0bcfd5 [Modified the version ranges of some dependencies. Nils Anders Danielsson **20120103205601 Ignore-this: 9aef21de942688c7a268d35c78715538 ] hash: 0000000497-518a98d5243d1a5b7d666ff493055cbe170d6bf78808be47f3f9c1ac9c5a8bda [Inlined some helper functions. Nils Anders Danielsson **20120127132635 Ignore-this: f636ab597e504978033629ef1d9f47fe ] hash: 0000001969-fb0aa6e39b7df57cc67779e09f2c9e460136a53f594fac1883c7d1e513afcc08 [Cosmetic change. Nils Anders Danielsson **20120127132700 Ignore-this: 490f9fef88952773222104bbf6672f83 ] hash: 0000000287-a6b8b09f3be12d8e261d21acffffbedfe9bf88a89980340bc796b3c6ca8dee5a [Added readFiniteFile. Nils Anders Danielsson **20120218111803 Ignore-this: a14d41344042cf41a5438af1f9a111a3 ] hash: 0000003702-1f232b4196ae58dc044bac056e391ff1ac352bbcd6927ffc56160794272e6ebc [Updated the copyright year range. Nils Anders Danielsson **20120225110204 Ignore-this: 1caec758d1560c6f13c613d77fff6f39 ] hash: 0000000318-2b668fb42b9006392da923207564d2f43798169f67f359bcebab04d7b56b3d7d [Added postulated, partly computing quotients. Nils Anders Danielsson **20120225110453 Ignore-this: dd2535cbffd5dfd4140fb004529e7886 + Implemented by Thorsten Altenkirch, James Chapman and myself. ] hash: 0000006473-6ed66f3fb0c2eaec33337f218eb8fb5172a1e22073bd904e3ea2e4a5ca478744 [Added _≡⟨_⟩_. Nils Anders Danielsson **20120225212140 Ignore-this: a22270b495981c2de38fed71532453a6 ] hash: 0000004991-40ad219ffb38ba7b71aa57ab4d986eb640f9065dbe647e46397b2fd9ff05a894 [Added idempotent. Nils Anders Danielsson **20120306141152 Ignore-this: 25563e42aae9e0dde988bfde2721eb5c ] hash: 0000001346-1d8b3472265929b9815eb59658e7d525d45b0c0d79b76b6c12f947a9a1e06e9b [Added _⇓. Nils Anders Danielsson **20120308131926 Ignore-this: 94c881424a838498d14d27b142b05fe9 ] hash: 0000000299-680eeffe98a86313cc536f72d2096a7039ba01f81b70ef432f26fec2f726f26c [Added Category.Monad.Partiality.All. Nils Anders Danielsson **20120312105757 Ignore-this: 76cd481222bc410f2fb60270d86c14ed ] hash: 0000006900-9dcc8f763df78c61943682606d8cb4178f818fea3b8e26704b0abbb1160863b6 [Added type signature to comply with new occurs check (issue 585). Andreas Abel **20120313164937 Ignore-this: 4f31b727f23d550a3f44a2040fff5449 ] hash: 0000000365-35db817b44988081432c1839eaf251b41f8ed1e9cae7438f8329258dcd4489ef [Added the irrelevance axiom. Nils Anders Danielsson **20120417083117 Ignore-this: a68d5d3274638dd650162685450bb04f ] hash: 0000000867-138e76395f4603484c8be50e0a2caab423e250bc03ea35872d4a228a927760d6 [Added Data.List.Properties.reverse-map-commute Joachim Breitner **20120507085543 Ignore-this: d1db66bb52a59967678f32fb25fc1102 ] hash: 0000000828-ed64c85383c00cbd8d532a0df42c8d76abdd4682354845a370e85678306ad7b7 [Added reverse-involutive Joachim Breitner **20120507085637 Ignore-this: 3606402188de305375b876f6890ab927 ] hash: 0000000758-0ae05d997fe74723cb60643893fcbf8b8ed2830292f7ba3420a90cd462cee945 [Adapted Joachim's patches to my taste. Nils Anders Danielsson **20120507094643 Ignore-this: b17198b645624e3c45929d2deacceec9 ] hash: 0000000731-29d5530036471cd4fb737d33df75956f64649c8fcff31f6ea7650385fa0e8b43 [Listed Joachim Breitner as a contributor. Nils Anders Danielsson **20120507094709 Ignore-this: d9da0f49ef2fd60caa084670acbb1786 ] hash: 0000000803-64ba04e6a104e88efda17042a3ca2d6f119fab56ec1f513da3cea2aa238ec479 [Relation.Binary.Vec.Pointwise: generalise to REL where possible Liyang HU **20120316110801 Ignore-this: 8df37c48fba43fb25ca50ddd9434c4c9 ] hash: 0000003390-70fe22d8ef2568d99ab79c7e8a41a8b7bcad093fb651c97e314f1c715ce1a168 [Relation.Binary.Vec.Pointwise: decidable{,′} for Pointwise{,′} Liyang HU **20120316110822 Ignore-this: c9abfc4fefb59277eed9e44ff20a1445 + Bonus head and tail for Pointwise′ ] hash: 0000001696-2ed1394010791be2ba0c7b7c64e6b18bd7906030ee901e79e0f3bcd9a3f462d5 [Data.Vector.Properties: lookup and _[_]≔_ behave as expected Liyang HU **20120316110701 Ignore-this: c79fe10e54fa8def528e31d688a2f660 + lookup∘update : lookup i (xs [ i ]≔ x) ≡ x + lookup∘update′ : i ≢ j → lookup i (xs [ j ]≔ y) ≡ lookup i xs ] hash: 0000001205-0c51a9e9beb72838c896c3cc3bf358f0a1f56d39c6b51227a6291882ea5174b8 [Adapted Liyang's patches to my taste. Nils Anders Danielsson **20120507124800 Ignore-this: f23fcf7f8cba245225710a4a9b7a8162 ] hash: 0000014494-c67ce420c50276919643bfdd3c9d1fb588245d23c1d40f36e3e572e0eb4e5029 [Listed Liyang Hu as a contributor. Nils Anders Danielsson **20120507125057 Ignore-this: a0489a5fe536a9aa87c6d824f7400157 ] hash: 0000000724-fdf23e701f7ca75d0e14251e8f7bbf9fc0df6f8236ed84d5a04def43ff3141d1 [AVL routines: added map, insertWith, union, unionWith, unions, unionsWith noam.zeilberger@gmail.com**20120429110436 Ignore-this: f7707bda509d0bc5e48e62bea59b51fe ] hash: 0000002068-a6b637cf81858419c8a5d38b30420d9d0ed9b3fc8fd790b5cd746840cde1a18b [Listed Noam Zeilberger as a contributor. Nils Anders Danielsson **20120507131227 Ignore-this: 1d1e23eeab0dc822594a9825daea7ef9 ] hash: 0000000512-4857a4cff964097d62d09da3270d5f00ab0039f22d4d01d77d71b1fe36f6cab5 [Adapted Noam's patch to my taste and fixed a bug. Nils Anders Danielsson **20120507150822 Ignore-this: 9b7fcfa80e62040e25a97548fb7d1af5 ] hash: 0000004460-d20dac75ecd143f06d70e334c320adf7af63d73d2c4530a7454d83a1791fa41e [primality implies coprimality gergo@erdi.hu**20120506122635 Ignore-this: a65431b2fa4a0d976f6fd4ab81cb8e7c Proof that prime numbers are coprime for all smaller numbers ] hash: 0000001590-0f1875ed242f480c0f53effa8d72de12c5abdaa758b6eee86675129afbed7a14 [Listed Érdi Gergő as a contributor. Nils Anders Danielsson **20120507160359 Ignore-this: 82f7bdc153d6e720a472a8557b8c2545 ] hash: 0000000727-c29abc428e68d2b908f6a53380d4495e6c62965bdffd6cccb1897720f7d165c1 [Adapted Gergő's patch to my taste. Nils Anders Danielsson **20120507160750 Ignore-this: 811c6d096fb79afe132b73bbbe7dbc60 ] hash: 0000003013-600f116c803d06dba03692e7925af3b76ef88bc37849ade0c8adcf12de6a0cdb [Replaced --no-termination-check with NO_TERMINATION_CHECK. Nils Anders Danielsson **20120418095116 Ignore-this: 77deeecfa1abe5aa590df671c913ac3 ] hash: 0000000300-68582d9e767d652223f3f629955671284c47e7cdb051696453e7cb2e2f6c7dad [Added i*j≡0⇒i≡0∨j≡0 to Data.Nat.Properties Joachim Breitner **20120510094133 Ignore-this: e7d50186d5a2a2c4246e21bdce7ab6bb This goes well with i+j≡0⇒i≡0 and i*j≡1⇒i≡1. ] hash: 0000000554-354634f3c3ea7eaa8f2447a047ce8ed36335ba5e6f7a206d23a4413515dbcc99 [Added toℕ-injective to Data.Fin.Props Joachim Breitner **20120510095237 Ignore-this: b1bf2333914f4fc13559ea732f5f25bd ] hash: 0000000524-edfe31882401841e33333b97933188ffc5e00641638906456443bf9062ba05f9 [Added i+[j∸m]≡i+j∸m to Data.Nat.Properties Joachim Breitner **20120510095820 Ignore-this: b438986ce991c51984487bd6b2ffc0ea Which goes well with lemmata like [i+j]∸[i+k]≡j∸k. ] hash: 0000000795-fac6f2332053141034bef32134920ff1f18a754451f7069a8d60af06f2ba4486 [Two lemmas about the monotonicity of ∸ Joachim Breitner **20120511091215 Ignore-this: 63c764bd45f4804dfe747a99a48f71e0 ] hash: 0000000709-2cda9173ef0c72567ffd0a39db999e9e87fe41f371447f384364388b6f14b1db [Added n∸n≡0. Renamed i+[j∸m]≡i+j∸m to +-∸-assoc. Nils Anders Danielsson **20120515142949 Ignore-this: f442f0811d5ce13f3bb127b6906a3781 ] hash: 0000002759-86daadab4130c23b93da7ee292a3ee588bfec4b908b881ef1451579df9f6a208 [Replaced ∸-mono₁ and ∸-mono₂ with ∸-mono. Nils Anders Danielsson **20120515143004 Ignore-this: eeb39c5ff560cd4f1979f98ae476c8d3 ] hash: 0000001125-feb500d2092a28dac7721289340c0afa338de90991730af76461e3d1933978b4 [Cosmetic changes. Nils Anders Danielsson **20120515143505 Ignore-this: 85998a1b0aa9ebbceb47a0f69adafac2 ] hash: 0000001631-b25472249e52b245d6635beea4a9760a1dc3d19653383679dabc11cadb59f77a [Removed the postulated quotients, which turned out to be unsound. Nils Anders Danielsson **20120516132746 Ignore-this: 59beea0edf033b56843cff95b9e5290 ] hash: 0000006671-4401d2501ae67f68685dbd0a281a05f88e3d598cf3b1283a5c7dd6742d4d4271 [Generalised Relation.Binary.List.Pointwise from Rel to REL. Stevan Andjelkovic **20120515184226 Ignore-this: 44eb5ba7562ddc445a86d3e3cecd6f94 ] hash: 0000012535-a660733608944ed65cc80ae514af766fd02d6c6991ff19e0b2c9afb11af725e2 [Cosmetic changes. Nils Anders Danielsson **20120516173847 Ignore-this: 77fdc80d47930231c701149a4e869d26 ] hash: 0000001583-7250727c4720e0af71fe5f9ef7778e22e0f826a976af8a6176b7258c5ec8fc8c [Listed Stevan Andjelkovic as a contributor. Nils Anders Danielsson **20120516174739 Ignore-this: 46edec47d470a1e882d5cc6d0cad76f1 ] hash: 0000001047-66b2eaf0cbf9efc26514fe49a842d6bb27f756250c60212e75735fbfda9e3bfe [Support for base 4.6. Nils Anders Danielsson **20120817222918 Ignore-this: 4a6777da48ae6e38237ed7dda511000a ] hash: 0000000481-3ac6f0a38b0bd1581c56ea33519757ce822c29a6cbbc8dd49dd63021b8a1fb18 [Added some hidden arguments which had been inferred automatically before adding polarity 'Nonvariant' to Agda. Andreas Abel **20120918125620 Ignore-this: edb56fcfeae48ec81c35ac8ba63816e8 Affects two files, roughly 6 definitions. ] hash: 0000003067-069f8958355caf72dad3c3e00910dcdb863ed53ff540f1ed02559f4abe89b8d3 [Adapted Andreas' patch to my taste. Nils Anders Danielsson **20121003141533 Ignore-this: 3500190b431004b1a441c1e114d05c81 ] hash: 0000000615-02d06e561ecb1c68413f251bf76401b19db52a602e43fe3e384fc2a68d9dcb8e [Made ∶ (type-signature) right-associative. Nils Anders Danielsson **20121023082544 Ignore-this: 40f2b00084510f2fe67eff07cf2e0a41 + This change was suggested by Dmytro Starosud. ] hash: 0000000295-955b0a7f81a2569708acd0e399d0a7cd08c6de2b5b0aa5e8e38a3d3994d34018 [Removed lots of dummy modules. Nils Anders Danielsson **20121101152328 Ignore-this: b07d9d0e5683a924c2782f47f7db9093 ] hash: 0000003740-c948e1b9437110500902d69f0e06aa05fb720359395bd0bd8de9d2a933ace525 [Added split. Nils Anders Danielsson **20121128174333 Ignore-this: 8aa368ca0a5375318ffec37f25032973 ] hash: 0000000586-c84bf4ed564a3f7afdf0560d4aff066fac3aa6751965e9fc38338b2388228a29 [Replaced the syntax Σ[ x ∶ A ] B with Σ[ x ∈ A ] B. Nils Anders Danielsson **20120506171416 Ignore-this: de9703959a0f42cf81466c21c4a22a9 ] hash: 0000001208-497fb9c19b31ecd8b26fb2cfcae97da188c3bc1bba8c4187cbd0b2f9a5c130ab [Added 2^_ and ⌊log₂_⌋. Nils Anders Danielsson **20121128185730 Ignore-this: 9a6aa6284ab597770561dd67d6b01a1e ] hash: 0000000432-ecce714009966eee0a1ff62b17211db9cae70e2f2978f8fc82e7f4aeec387b8c [Renamed _∶_ to _/_. Nils Anders Danielsson **20121128185933 Ignore-this: 7feee4f6ecd7a4f53ae03e379175ee61 ] hash: 0000005651-199f573fadadd734110772b7679743533cdb123e7bbf4bf2eb1fe04e0bfd2bb2 [Removed DivMod/_divMod_, renamed DivMod'/_divMod'_ to DivMod/_divMod_. Nils Anders Danielsson **20121128190917 Ignore-this: d390430e62e892072f24f1c5d6465a6 + DivMod was also turned into a record type. ] hash: 0000002940-f2c65f2e36cb6550a95ec14a9c356807a3899cd4cea6c73f506bdd64e5d4e04b [Removed Digit and theDigits. Nils Anders Danielsson **20121128190932 Ignore-this: d18c7111b283978ccf62fb8688a2d71 ] hash: 0000001852-af7a339b8ac91478b956c279b1def0f96539a76a2e081667012a8a5bee6e216d [Renamed type-signature to _∋_. Removed the "x ∶ A" syntax. Nils Anders Danielsson **20121128191243 Ignore-this: 6802ba5bfe7fcb3e97bad06a82dd8ce1 ] hash: 0000001846-8230b9d5e72b700b16b06309b19658c841db4bc9273d06fe4f0a0c5c941e060a [Added ×-homo-+ and ×1-homo-*. Nils Anders Danielsson **20121128191504 Ignore-this: 182bbb6e3950f7a0e964cdb179b93bca ] hash: 0000001703-70b3f570ef83dc3e147ee8cfe52897e00b6270a1ea636994f21506df3eb4d999 [Added _≈⟨⟩_ and _≡⟨⟩_. Nils Anders Danielsson **20121128214911 Ignore-this: 2ae3fd0f581e3b6b891c77bc49dcee30 ] hash: 0000000891-3540e64b48fb87a8f717747df019a0a323eec22d3bb2b39a70e7a69dee5c5eed [Changed the definition of _×_: made 1 × x definitionally equal to x. Nils Anders Danielsson **20121128215043 Ignore-this: 7ae69e18a608e64c22666b64017029fe ] hash: 0000001957-9f6ca5125d1514bb6cd48a099b9eb2f672e8a26d35ed18e8c7155f42de590051 [Added Function.Related.TypeIsomorphisms.Solver. Nils Anders Danielsson **20121128215152 Ignore-this: d5a0d02822eac73eb7fa029ba8e3823b ] hash: 0000002890-2d51eae03723ef1d8353baeac619dde5e2ed036b3d9774f2c0642f9a28e71031 [Modified a comment. Nils Anders Danielsson **20121128215203 Ignore-this: fb2897cfee37e1a91a48c9767eab9fb1 ] hash: 0000000303-4bf5e9ffdf79e45e65222c4ca0023164d7af7e7e7d02ebe67fc2291f31e44637 [Added Σ-syntax. Nils Anders Danielsson **20121221055827 Ignore-this: 6682d4567bd22a83e6a5986a7db2c3ad ] hash: 0000000478-2f10f862d0314f576cf8012044a094e72d120f63e9cca2ffab1ac7fc4ce68583 [fromWitnessFalse gergo@erdi.hu**20120518150707 Ignore-this: 9c17add0930b4b5da46f814242087cfc ] hash: 0000000301-41be7dfbef74148f0bfb2d1946b25f9560b2928c4fc9cf071d644f652573953b [Added toWitnessFalse. Nils Anders Danielsson **20121221060447 Ignore-this: aa4c35fd3fe488f5c475ed9a6d338ea6 ] hash: 0000000361-730498f627894641062f21e442aacae50a08f7943d10d8c10c0bf9b6a3b4fd14 [reverse-involutive ERDI Gergo **20120527134925 Ignore-this: ef1127d23c8aae6af1f58dbfbf60cbab Reverse is involutive over Fin n ] hash: 0000002442-3172c14ee6eede7443de307e1790b771befa3fe08d696cb75272b58c502bb16d [decidability of implication noam.zeilberger@gmail.com**20120523191557 Ignore-this: a6c25a6a4dceee3b8c5e0a45eb7afd06 ] hash: 0000000844-413e09f6a399371b536ac46bbc621ed183e4e64dddfc337d35915a22c3c81a37 [added unzip for Vec noam.zeilberger@gmail.com**20120524124230 Ignore-this: 15cca3fb128484d647171f21159315bd ] hash: 0000000336-59c12c755929be2f2524edeebb7e410c3aa7cf4017a97b683c8278a7a0fbe970 [Removed the use of "with" from unzip. Nils Anders Danielsson **20121221062927 Ignore-this: 6c7d84f8d4af98ff99a2d66644b70a9b ] hash: 0000000389-ba93df051ea5d2c0ade114e3dc41b78ef39e4ef9dd690fce94b6482ed9cdaf00 [Add M-types module (dual of W) and define least and greatest fixpoint for containers using W and M. Stevan Andjelkovic **20120820111849 Ignore-this: a0f26d2bbe36b66366ed27ba12d0baa9 ] hash: 0000001270-421fc5c107214f1fe0a108256f993834a6ad945c643b7484606fe9d5852658b7 [Cosmetic changes. Nils Anders Danielsson **20121221070529 Ignore-this: 8c86eac13832fa69701e7d36650814f1 ] hash: 0000002220-8cf00d231dde52f6465437d9d7a94b86bd25de154ccd9909bdebba339f9f6757