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