pristine:0ddb61fdee9de484140d541a57d769853a4c6b121433d99de841d4b128b4cd34 Starting with inventory: 0000019539-b9e82ce3cfcac8c83d406f8b739f76177369ad2d02d3d734b4318e581f344919 [TAG 0.7 Nils Anders Danielsson **20130129162215 Ignore-this: 279d0b14ba997458df89073da57ce50 ] hash: 0000013259-2ab5dac9dc343ab4ca7071585f023ed3c0a2a0d72178539f232ac80ef0d626ca [Removed release-specific information. Nils Anders Danielsson **20130129162230 Ignore-this: f960b19320bf282bdc03b1b8e3d561b0 ] hash: 0000000612-6b1cd3a39c21a0124c659dab9a27d3736f270d0428e923006ec4d2d66610e903 [Factorize Arg. Guilhem Moulin **20121116204148 Ignore-this: e4c5a0d7cf3a50c97826f4c7cf734140 ] hash: 0000002488-0cd249fad06532c508af3b3f8d01cf44ead67df6cbb81569f94c014ac6efae78 [Included Guilhem Moulin in the list of contributors. Nils Anders Danielsson **20130220104515 Ignore-this: cd79a3214fe4b4d41ce47881dae5d98 ] hash: 0000000504-5c5448257a124db65abd7ad3d2d3f4cb0c9ef5f3b8e7f9ce7ba6214bfed0cd6d [Renamed ArgInfo/arginfo to Arg-info/arg-info. Nils Anders Danielsson **20130220120912 Ignore-this: c7dad0d4e2d9ed4df5a7f9e13b442 ] hash: 0000002281-c7f43776cfbd7a7fd274712ac47fcef59c27caf416f22e4d478b05b5ec3817af [Added decToMaybe. Nils Anders Danielsson **20130222171834 Ignore-this: f1cd1b105af163a8c5b6e8da4ec6af44 ] hash: 0000000409-faab2ddce6de1e0776dc82eb0704d55a74730538ecd19674a91dfdb082b3111c [Added Data.Maybe.map. Nils Anders Danielsson **20130225095411 Ignore-this: c9a389f7f021a8190cfa3e21a50ea3aa ] hash: 0000002169-ef230a373f54fdf205872baa9299d06274efd9a31f6fc4e49556e1460b667eac [Added Algebra.Monoid-solver. Nils Anders Danielsson **20130225105203 Ignore-this: f232c003a2bbd1927c8e75e697eae5e5 ] hash: 0000005714-516b625f6f6438b876dc63910b7dde7409e30dc5aecf25d9622aa49560dd0994 [Added fixity declarations for _¬-⊎_ and _⊎-dec_. Nils Anders Danielsson **20130225160336 Ignore-this: 5b5bbdcb25d8a7f58e211719df537d7c ] hash: 0000000248-e8ac2eebd914c01d626994e4ff9d836ef074da60d76bff35b0c7770c68215c1c [Added T-not-≡. Nils Anders Danielsson **20130301094556 Ignore-this: 809f65054fd98067498249d1b53c5ff2 ] hash: 0000000345-fecea593dfe0141b628fa2ad11c35a9a50a7aaa0a831fc225bc4aff27d01ddd4 [Added split and wordsBy. Nils Anders Danielsson **20130301101819 Ignore-this: 3f0ddbe73af6ad6ef963cbd3b5362e57 ] hash: 0000004370-05354a9cb4644de849a62b71b6027d0ae50ba85735688a338a15b71616eaa777 [Added length-replicate. Nils Anders Danielsson **20130304133916 Ignore-this: 45a1bb4feec59bc27c48e19b009cb9cc ] hash: 0000000386-342d55b47ea304ff18f7f2d7ca3c9fa42fe230192fb3f9019599fbb045d2c124 [Made _⊛_ less "strict", as suggested by Patrick Palka. Nils Anders Danielsson **20130304184208 Ignore-this: 374079025b60c6f877c4db0c86d56b4c + See http://code.google.com/p/agda/issues/detail?id=673. ] hash: 0000000323-206d856d3288e6df2f275410c45495aa9da4579705a60df1f65fef058bf0ed8f [Defined Any and All using recursion, generalised their types. Nils Anders Danielsson **20130306114412 Ignore-this: 461ba6cc52988357b07f9b474729ab23 ] hash: 0000002167-5c59afe3e68c7637377ebdba64c795f65c8abdaf1511230deeea4d73cb353f24 [Added toWitness. Nils Anders Danielsson **20130306121234 Ignore-this: b487512ba93fb09ad03db1b490d9a4c1 ] hash: 0000000303-5d8b146000913336c8e5102fdbb12dd740fc1c62b92ccb79afa661c3f7d4d343 [Non-empty lists are now represented by an element plus a regular list. Nils Anders Danielsson **20130306233137 Ignore-this: 1a504fd07418c43ffb194dc8dc9f4e5c ] hash: 0000011985-7e0f03f4f806d01b4d53fccad7e8e84330254ca597a2bf27d72897d157f8d8a2 [Changed the fixities of _∷ʳ_ and _⁺∷ʳ_. Nils Anders Danielsson **20130306233215 Ignore-this: 493c7b735ea43f59ecbcf96ee97419ed ] hash: 0000000268-a2d39a77003546010cbd5fd69c09cb8046599b07f7fc23478b7ac01d0194c518 [Added ∈-tabulate and ∈-allFin. Nils Anders Danielsson **20130308183949 Ignore-this: c36e088ad4f2c575134a4829b38bf307 ] hash: 0000000540-73949314d3826f02a16e27f71231fab8fa77ac9cd81cc6a3e170cc0620c0abfb [Added ∈⇒List-∈ and List-∈⇒∈. Nils Anders Danielsson **20130308184004 Ignore-this: daff0f39f26f91abac04f3bb261cb328 ] hash: 0000000860-e23080f6ec75cab65496631b2e293075ecca7ddf4a11846f7391540316a1ba2d [Added map-Decidable. Nils Anders Danielsson **20130308193926 Ignore-this: ab21edd839d9b082d7ba0988b936e23e ] hash: 0000004074-66d4bd22234606b68843d6f8b457044303ab6fdbe59cce3e782441ea4d566dd3 [Removed map-Decidable. Nils Anders Danielsson **20130308215557 Ignore-this: d1a4b20bed5fcc8d1b637c46d319b90b ] hash: 0000004077-709d6241449c7dd80e2ef9204c17ceb7049c6cf7a312f47dac2133e2876a0ed0 [Replaced length_-1 with length. Nils Anders Danielsson **20130309190315 Ignore-this: bc2639fc3bb47820e79ca303dc0b4a1a ] hash: 0000000562-0d10abe0e6e8e092d384062c1098df9be054682687860a37e608d63f13dea590 [Added True↔. Nils Anders Danielsson **20130312170441 Ignore-this: 6a1164d6ce6696fbdc006993d31e0cac ] hash: 0000001061-1ee276bc508d66b73dc75fb6cffcb56c2cc2ba21b4b87349ed3edab1f10cc6a4 [Changed the definitions of Data.Char._==_ and Data.String._==_. Nils Anders Danielsson **20130322194110 Ignore-this: 170812374abd7f3e69349b1e56ba87f4 ] hash: 0000002156-ce1370e0c554bb6401c85f4b5c4885e6e1fca7b6fd9fefb805b06f67d240637a [DecTotalOrder for Data.Rational Noriyuki OHKAWA **20130412165805 Ignore-this: c279af5e3405e2b0cc53c15054c29382 ] hash: 0000007443-fa7c21843c20ec38c83200b06e7cc117017410338deff8d02276aeed5011b3ca [Renamed p≤q to *≤*. Cosmetic changes. Nils Anders Danielsson **20130417120225 Ignore-this: 4b6805587d4d3c260a976a6e097ea271 ] hash: 0000008344-7a416a514041d13a65618e79ec2df0a21dc8a4b7a06d0b4f5051bff24be4e984 [Included Noriyuki OHKAWA in the list of contributors. Nils Anders Danielsson **20130417120416 Ignore-this: 6d0285bdd38946ad4f91cba91ca64b07 ] hash: 0000000576-52dd80b41c84ea0a53415b5754f7eeda963d61fcdebbc09d1d4637c9777af887 [Equality between pairs can be expressed as a pair of equalities. Stevan Andjelkovic **20130418172817 Ignore-this: a8d1aa3a2a9612d5fed8ffd03ccbc868 ] hash: 0000002779-283dc087e70ca4f4be2187abf0ce287ad55fa47038f4253d9cdeaca13929d944 [If the components of a sum are decidable, then so is the sum. Stevan Andjelkovic **20130418173414 Ignore-this: a6ad623c32d6d3eccf54fbe8cd841bcf ] hash: 0000001522-71c6fc96057b34a9d7f5a46fbec580f567205efcad68bbbe01062d6b20f369a0 [If the components of a pair are decidable, then so is the pair. Stevan Andjelkovic **20130418173608 Ignore-this: 978197561edc8bef0b5fe0411971ab1e ] hash: 0000001488-040ee807b01ac3d95adb49e3d3c69104b4b14fab9de72719c6ab1e3f8184040a [If the components of a list are decidable, then so is the list. Stevan Andjelkovic **20130418173848 Ignore-this: 17b57098ac7ccee1052ab68b4e956367 ] hash: 0000001155-38238cbf4b3c769459439208f020eabd3eca5e59c33a81c47279267b5ba4f4fe [Add map-injection to Rel.Nullary.Decidable and define {Nat,Fin}.eq? in terms of it. Stevan Andjelkovic **20130418172516 Ignore-this: 76e35ec2ee820cdd7debb79f3aed1f5f ] hash: 0000002575-b25f94e9418905050439a068f89f98a0b7a771f0207d206f746e06a8387cd59e [Renamed functions, modified comments, made cosmetic changes. Nils Anders Danielsson **20130422162538 Ignore-this: 74fe7dd03a318ce055561740b886eb08 ] hash: 0000011684-ee13b58a524813eea386eaaab66aa99db88ddbec112deb8fca2a5e63bf699433 [Cosmetic changes. Nils Anders Danielsson **20130501140641 Ignore-this: e07906ceef46b56b50d6ba4984282b5b ] hash: 0000000419-060e72165762a0e19d376dac2c13fe9e976fefe7010bcf04f9cacf57ae988bd0 [Add the free monad construction on containers Stevan Andjelkovic **20130529144328 Ignore-this: c8366cf0ad47683b455f73f7b65216eb ] hash: 0000001695-3386ca38cdde09a1f751168872760227b1fb7d361b0e42d3b73e5720b1632e77 [Added toList∘fromList and fromList∘toList. Nils Anders Danielsson **20130307141439 Ignore-this: f5a0170c38cab12f64ad70e821753bec ] hash: 0000000381-93512d5f71ad80ee4fd4801b99d6a925e487aabd81667d50aa99baa701677617 [Changed the type of _≈_._∷_: the first argument is now an equality. Nils Anders Danielsson **20130314224240 Ignore-this: 7e4bb33efa329aeebddb3a75b6076030 ] hash: 0000001440-b0597af2ade9538e01757f56c7a7ceb9dfcf152ac9f5e13b848b2672c2f72d0d [Added head-cong and tail-cong. Nils Anders Danielsson **20130314224248 Ignore-this: 7178c5cc27fa524481b96a6a1340bb3 ] hash: 0000000615-39f6c2057d6c6d6cbc917c1f8a60c86e32ad4f84dd72b8ec0d3b77157dee4bfa [Added push-function-into-if. Nils Anders Danielsson **20130610165059 Ignore-this: c08fa801383bbfb6b72c609c6f27c5ee ] hash: 0000000418-b60c64df1ec5e6fac58b3d7a46aa9547161475695b15f6f30df9fa5ff92601df [Various changes related to Any/All. Nils Anders Danielsson **20130614145219 Ignore-this: b00ebcbe82a5c0a1c376d767c483d77f + Defined Any/All as data types. + Renamed IsJust to Is-just and IsNothing to Is-nothing. + Renamed maybeToBool to is-just, added is-nothing. + Changed the type of toWitness, renamed toWitness to to-witness, added to-witness-T. ] hash: 0000002992-77dad5b8573880b95bb58c9e27225d6d339fa828b21a858722f020ea2d824281 [Made Induction.* more universe-polymorphic. Nils Anders Danielsson **20130715215543 Ignore-this: 29cccd9e5e29e7dc01b5b7b1be31c44a ] hash: 0000007570-40286c56592a3f733c6979780b4a696f52206c6ad99fdc664b39eb0f190ba8f1 [Added more examples. Nils Anders Danielsson **20130716131933 Ignore-this: 2b7b978d42d18805dd0b3f4704d27590 ] hash: 0000005840-3b835d13902f7c3ddfa8380c385d2017c699a60d437f06c14c3f80c7b9bbcadb [Added EquationalReasoning._↔⟨⟩_. Nils Anders Danielsson **20130716140543 Ignore-this: fdfa8a8ae69680a6acc733df9c8eb09e ] hash: 0000000479-4ac20f53c59cfbef0fba5fe012407fc067cfa30c6b027eb8dec06a003b0672c0 [Added Any-resp, Any-cong and Any-∈. Nils Anders Danielsson **20130716184040 Ignore-this: 42c7562f44bcdc02422aecd854e95d82 ] hash: 0000002964-cfedbd43bb1ebdf5b2c083f83acede7958dd94d7b59749c57b9dbcf6bb0eae35 [Added index, lookup-index and index-Any-resp. Nils Anders Danielsson **20130716184632 Ignore-this: 2e631da4338ebc8160cf1f8fbb8ea753 ] hash: 0000001299-7da305c2f17c3f13ab66d55f7c5ab6ec99925e9f4168b3fd71730affdcea6e45 [Added _⋎_, Any-⋎ and index-Any-⋎. Nils Anders Danielsson **20130716185048 Ignore-this: e21c5a8397ca0637885774ff6b95ed73 ] hash: 0000004779-78276f8858c31038aeca9b270a92b8295372cbfd90f6ca9e7a506f9b3b6646df [Added Data.Colist.Infinite-merge. Nils Anders Danielsson **20130716185501 Ignore-this: 7572da5a0b02045f4a1f2b9df58ece5d ] hash: 0000010540-314b78205fc847d587ef323638285368fbfa317130c68cfb5d0a60308b823095 [Added Any-map. Nils Anders Danielsson **20130727174001 Ignore-this: c46bb151f372eed36c04e4efea502321 ] hash: 0000001410-a3d8d5042e1b18bf714150b1fe7a5e05dd8a5e47b55f84dd0f1563eee5612121 [Made Any-resp and Any-cong more general. Nils Anders Danielsson **20130727192306 Ignore-this: a22306ba40191f95a2488893ac1913a1 ] hash: 0000004311-7bc66d08b152034f95509508a1dfc7df62240ad754a885cd6b053d9331c28e6f [Changed the definition of _≅_. Nils Anders Danielsson **20130822132326 Ignore-this: 20dff8b5195dbf52dbd8a44f90fb754e ] hash: 0000002994-e5eb36b8a378addd934afd3374e864170c97c9e53249cbf1535987c9825e9fe3 [Added three lemmas relating Any, All and negation. Nils Anders Danielsson **20130919133202 Ignore-this: c30481fa6202bae476eb486afe0f8306 + Sergei Meshveliani suggested that one could add a lemma stating that All (¬_ ∘ P) xs is equivalent to ¬ Any P xs. ] hash: 0000003274-8893b9c67e76ed3c00fa96fe888ad679525399a21779cd95fc04a29a3e054161 [Modified a comment. Nils Anders Danielsson **20130919133413 Ignore-this: a7219685fd09780fe431b6dea99a2799 ] hash: 0000000270-83bed2acd5d9bdaa792f4b5551d3452e13ad43296d798fd1ac98e3b6bd93ca91 [Added StrictPartialOrder.asymmetric. Nils Anders Danielsson **20131104172352 Ignore-this: f3d190c8b3fd85daab5a3c5f2aab1dfa + Following a suggestion by Sergei Meshveliani. ] hash: 0000000363-24e3d938784074ab48db664007f1e9050f5bb0aea64497c693bb5fd9f16f6cd3 [Level primitives have been moved to Agda.Prim. Andreas Abel **20131102190148 Ignore-this: 6de95720338bbefe7eb4cbb473419d4a ] hash: 0000000801-decf776f798b2b0fcaf4f56bf9eec5c461aef9cf708f259a89bb06c060889a96 [Agda.Prim has been renamed to Agda.Primitive. Nils Anders Danielsson **20131115135749 Ignore-this: 6b0c11ea50fdd88a987fa7241e6904d2 ] hash: 0000000259-6c2f50c51e6d2b9435cc05ac1d03d0ba348a7c1fdf94a41480a3441c84f6bb37 [Modified a comment. Nils Anders Danielsson **20131128142907 Ignore-this: 7091674eb53b18d2785ab40bff8c5812 ] hash: 0000000312-d7f9a8677028bfb07d32290469c0bfc88289c17fa824c0d001ed8ab46d68050e [Removed BUILTIN ZERO and BUILTIN SUC. Nils Anders Danielsson **20131128142955 Ignore-this: 96087d6c3fbf42b594f2e924ce4e7b86 ] hash: 0000000310-8ec4d26c70f125434630482f297989764e4a44d32cd8ecada7987d7eaad57d97