Starting with inventory: 0000018360-fb89e58b5232d4d99f9200d997e621e704b09f71a9b4f5d45382df50cef1e70d [TAG 0.5 Nils Anders Danielsson **20110220174322 Ignore-this: a1764929c4ac99fd89d977760b2815d5 ] hash: 0000012819-bddca1769e6b94ce02219e2ce5cbdc7de2e1757502bbed9425850da6e1ec0e07 [Removed release-specific information. Nils Anders Danielsson **20110220174348 Ignore-this: e9896e46d4e46d4d1b08d7abb34fd7ec ] hash: 0000000613-b8b4b30682a70da3ba81ebd78a0c445cfd69caba96864f8fe5f02be4af845df8 [Fixed a comment. Nils Anders Danielsson **20110310115657 Ignore-this: 106bb77d1e1bf6f7b04f9084032aa2d6 ] hash: 0000000331-5bbcf639397f86097ca83dd6bebf8ec474dd00ab56ce44072e8a004e0241e70c [Moved the Isomorphism universe to a new module, renamed it to Related. Nils Anders Danielsson **20110311095829 Ignore-this: b2a31c6851076cc5c2f990eb541a6e89 ] hash: 0000020975-a3edd277b154512647fb51d299da4d38bfa378be25d82e40e1051666f623eb39 [Removed outdated comment. Nils Anders Danielsson **20110311144420 Ignore-this: 3e204d5b95d7fbe5cf65c26784610b6f ] hash: 0000000419-927d4776fe1935ac50a8dc09a0e4e2199feaddf6869b045d144f47ec17dc6b30 [Added ∷↔ and ∷-cong. Nils Anders Danielsson **20110312135545 Ignore-this: aacf4a2123fcf6acd7a926a062ac0d16 ] hash: 0000001181-cdc553051bf791d0daa2585b3cddd44c78bc4a8e61b68dd268f258cf58a6ce8d [Added six new members to the Related universe. Nils Anders Danielsson **20110312235545 Ignore-this: 8decd734f249ee6992e2ecfa32c75f71 + Adapted related code and added a number of congruence lemmas. + Added the synonym _≈[_]_. + Added the wrapper types _←_ and _↢_. + Added _op and reverse. + Added some "subuniverses": Symmetric-kind, Forward-kind, Backward-kind and Equivalence-kind. + Added code for preorders, in addition to existing code for setoids. + Added the synonyms subset, superset, subbag and superbag in Data.List.Any and Data.Container. + Added Function.Injection._↣_ and Function.LeftInverse._↞_. + Added Function.Surjection.fromRightInverse. + Removed Function.Inverse.setoid. + Renamed Function.Equivalence.Equivalent to Equivalence, Function.Inverse._⇿_ to _↔_ and Data.Fin.Subset.∪⇿⊎ to ∪⇔⊎. ] hash: 0000123192-a707889d8283c395e994ebd5fa96e81000ddcaa5324f4de714a5d2a2bea05828 [Simplified the implementation of drop-cons. Nils Anders Danielsson **20110318162434 Ignore-this: 5937df1fa3e113823bf907fd69c5eac5 ] hash: 0000008444-967a0075f3ef8151bf6a0121db85f29322ee1a7d6e31c6ef495a8dc735950174 [Added an encoding of record types with manifest fields and "with". Nils Anders Danielsson **20110328142717 Ignore-this: fbed1d9d33485b031ee44975ef775b85 ] hash: 0000010754-6fd93bcd3c5a322ed35faf983adbf23d3ae17eae9c4b61af8109164199fb59c5 [Renamed Data.Container._◃_ to _▷_. Nils Anders Danielsson **20110328163236 Ignore-this: 7f9df5b1e61e2e4c6b4a4a0367d2e5cb ] hash: 0000001485-24d62a171a00988d4b6889c8aaa0e36d6e94552d77c1ad22b0cfd3dd275447f6 [Patched std-lib to work with meta-variable freezing. andreas.abel@ifi.lmu.de**20110411230625 Only minor changes like adding some type sigs and omitted arguments. ] hash: 0000003596-ed25675815b3ecf10d3ea6ff485938b580bfdb5f83be33a4fe5c714cc1f65041 [Included Andreas Abel in the contributor lists. Nils Anders Danielsson **20110412091843 Ignore-this: b4ceeaaf11205c535922280bceeab060 ] hash: 0000000791-519a434a5f8fd761c41a57177af19a1c50f4a89af06e8cb17cbb48015b614891 [Modified Andreas' changes slightly. Nils Anders Danielsson **20110412094133 Ignore-this: cfa931af3dc6d60850a4b1aa3b6cba81 ] hash: 0000002551-731c57c12f23d4389aba18a82bb7fb0123008d050d0c3673cc80bfbaa9d69d27 [Added Haskell FFI bindings to Empty, Level, List, Maybe, Stream and Sum. ajeffrey@bell-labs.com**20100930195706 Ignore-this: eabfce87191af369e276f9752b775085 ] hash: 0000001257-8468ef3e554da3f07e7dfd143b0294f306e5fdbf1a7f91748127976cada039ce [Cosmetic changes. Nils Anders Danielsson **20110426151522 Ignore-this: 496a4b53e21a5f6be6b35d1d91fccbe8 ] hash: 0000000436-643d56c6c4664ed70e2e921d97ebe4d8e789ab62ffc8f9bd6201ac1673aea670 [Moved auxiliary Haskell code to separate directory, added Cabal file. Nils Anders Danielsson **20110427120911 Ignore-this: 3c001a7eea8db5a161e92c5af55aa600 ] hash: 0000001712-0aae6d0c7b011194cb4a7e8e6775ce190e18359b8005d7e5dcd0485f057b1d07 [Listed Alcatel-Lucent (copyright holder) and Alan Jeffrey (contributor). Nils Anders Danielsson **20110427122814 Ignore-this: 4d5644a381ef89cef53c5580f3b6d641 ] hash: 0000000538-3b9088c013eb68f492aa916ec7329c10e7df09555141f1028747698e1af740b1 [Renamed 0∣0 to 0∣⇒≡0 and 1∣1 to ∣1⇒≡1. Andrés Sicard-Ramírez **20110427144030 Ignore-this: 38b19d98c90b2c2ff6f8c4bf58618349 ] hash: 0000000928-00b7ccd5ce41404fab39f3b5f5c4317bbb40eff0bee8c199fbb30c3e4ce672ca [Added COMPILED_DATA pragma for colists, removed Foreign.Haskell.Colist. Nils Anders Danielsson **20110427230507 Ignore-this: 98a38d13c045b25a991deca98a4e2b9e ] hash: 0000002348-992f39d9efd7d3468ca712c82fe68cb30d55e7d2591bdfe45e8318ba3ddff25f [Declare IO as a builtin (following the correspondant change in Agda) Nicolas Pouillard **20110414204004 Ignore-this: ca4eebf4105208d85220e7d7eef72b86 ] hash: 0000000243-6ac4347ac783244f67f2ad7874b4775f975d1c6af5814faebd8396e4ddc3d30f [Made IO universe-polymorphic. Nils Anders Danielsson **20110428164629 Ignore-this: 2be051bdca45f319922e10cce9d6009 ] hash: 0000003751-cd271eb33cc751ad4daba6aca6893db5d4353a3daa9e7217fbc7a882964fd275 [Upgrade the Reflection module to follow the Agda one. Nicolas Pouillard **20110414204250 Ignore-this: 83cec08e8112bd04dfe37d88799cb593 ] hash: 0000010766-e24af759abe869e281d61ab9c0aa18c35ab313884c2abb420a3acccdc7ffafd3 [Follows the latest reflection API Nicolas Pouillard **20110502221109 Ignore-this: b7d8b87a4e315a04d9a8f5ba71a10fc ] hash: 0000001904-b948efefc106623a9f2f407a1c61c9759ecaf41f76f0931fdf1b3ccab8c8c57e [Reflection: use better names for primitives (and fix the QName->Name issue) Nicolas Pouillard **20110504114546 Ignore-this: 62aadb600d8a09d701c728649a22aac5 ] hash: 0000000721-cbdaa4dec9b431227f3adf95d809efa11730bb9ed31a8659f6dac01541ba8f0a [Added a fixity declaration. Nils Anders Danielsson **20110504145027 Ignore-this: 70ec53b459ef2e2219bcb9f581a2cada ] hash: 0000000216-a373d02bf38220a457ae8becb1a7c3a542a99fbff6203258a8c7ec73f3d4adbd [Added support for instance arguments, renamed many things. Nils Anders Danielsson **20110506144700 Ignore-this: b513a3b0d2c77f4d868475ac8fb6f18c + I also removed all uses of cong₃, map₂′ and map₃′, because I decided not to push the patches which implement those functions. ] hash: 0000015565-9df85d0812518f638b41fee62c0842490ec5d1c60f72df09e14eebdd00bed8fb [Made Relation.{Binary.Simple,Nullary.Universe} more universe-polymorphic. Nils Anders Danielsson **20110517133603 Ignore-this: c7ca1290d2d4aa7b256727cb4f746f9a ] hash: 0000004067-b884deef4b61b1024d0454c2474d640dd5210939a1a1edd9e059674291fbb83c [Renamed _≈[_]_ to _∼[_]_ and _≈⟨_⟩_ to _∼⟨_⟩_. Nils Anders Danielsson **20110517212103 Ignore-this: b04202adc5805c355c49fca4057de3e6 ] hash: 0000015670-8d64dda6283ca9129b110c7ad384bc83c65c3ec79941c3c0b378bcadc563c00a [Cosmetic change. Andrés Sicard-Ramírez **20110520160731 Ignore-this: a985e1e16e770fe8765e648d36c1ac7c ] hash: 0000000222-e49aeccda1d93da91873c29975c113c1cee8e807da133df912704437a2c730e0 [Added _ˢ_. Nils Anders Danielsson **20110607140013 Ignore-this: b4117b45dedcc08c3af361684e27e6f2 ] hash: 0000000598-aabbd152f06f44109ba9b74bca3720fd331a3b69720bdb359004ef54cbde5f60 [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110607141926 Ignore-this: 8b12d164e668255aca6d215c31958269 ] hash: 0000000457-12d45590ef20098b67be4c042c3e3a299b2b0f3d94d4a386c0d7a37b2659d718 [Added ≡-Reasoning._≅⟨_⟩_. Nils Anders Danielsson **20110610113331 Ignore-this: 17886a98365ffe44366dbad2d6690276 ] hash: 0000002176-725af568af8c1eb20dd85d5d34eb749b95073d13042f613df2ee31e8ec485279 [Added some definitions related to functional extensionality. Nils Anders Danielsson **20110621210505 Ignore-this: e4ab5c057dfad1f118571e28e77102f8 ] hash: 0000002858-161751fe863954e514aed65b0716938cd961f7aabce9c1a9a9a7f3cfe95f2222 [Turned Record into a record type. Nils Anders Danielsson **20110622090529 Ignore-this: 8c3e59f5d1188a10a0f86b33a082a49b ] hash: 0000003677-e523abf5bfe30df7bd30b1bbac3be5095223dbec96fec1f5dcbb57a42b7b6280 [update to work with new level representation ulfn@chalmers.se**20110623081950 Ignore-this: 4129c1b2c86d5e0bd0e023070edf14e6 ] hash: 0000008797-8ee3cadd44046bad99dbc4332e9c81d65fb9961e5240af3728ea256e86c6df0f [Further updates related to the changes to universe polymorphism. Nils Anders Danielsson **20110623165938 Ignore-this: b1b1c4260209fc5da44f040048dc522b + Re-renamed lzero to zero and lsuc to suc. + Added a COMPILED pragma for Level._⊔_. + Level is now compiled to () (when MAlonzo is used). This should be safe, because it is no longer possible to pattern match on levels. ] hash: 0000010831-a349444a4ed10a35c34c0899f94f05fd4a101b09f637403a6f73660b8c8ab358 [Worked around Agda issue number 398. Nils Anders Danielsson **20110629132829 Ignore-this: 76a0d2b87b92a02a2d11bc78616d0bca + The previous implementation of showInBase could lead to a segmentation fault when compiled using MAlonzo, apparently due to a bug in GHC. ] hash: 0000000672-b6e843afd3ffe4f89a47e002d03e025809a2696b5681aefdc0d3691aad096139 [Simplification: Agda has become better at inferring level arguments. Nils Anders Danielsson **20110701155156 Ignore-this: 474e025e41e7c01ba2451663aa712238 ] hash: 0000003317-a63f357d650d6a444c5b74201f35e462fa45f84fdd11ee9e687ceaaa3d6d0505 [Simplification: Dot patterns are now allowed inside record patterns. Nils Anders Danielsson **20110701155203 Ignore-this: c403d338dbc48d54fa2da56bc5759b6d + Well, allowed in more cases than they used to. ] hash: 0000002540-0e35ab7966b04fd00572f53686971202618df3cfb92c153281f5f483ada738ab [Added indexed universes. Nils Anders Danielsson **20110705092723 Ignore-this: 3676411b8e4a8e0b42169d7146c3effe ] hash: 0000000695-14468e03e540ec02380905839d4c5de31005c7f67b8d18aab05a0c3942a49349 [Made trustMe universe-polymorphic. Nils Anders Danielsson **20110809095333 Ignore-this: 53b6e0a039167579f460a9921965f40e ] hash: 0000000786-c9daf740325ce9c975699aee083946b5b6eec9fbc04a0d663689ce4895830230 [Support for GHC 7.2.1. Nils Anders Danielsson **20110810134018 Ignore-this: cbb11f99baffa97647fb5925c40f2ab1 ] hash: 0000000359-64f538cfb8aae6e7adf5fd79bb420a37b7a4871fa203165238c64a9e61f5f3a6 [Experiment: Represented kinds with equality in a different way. Nils Anders Danielsson **20110830095720 Ignore-this: dc1bada90f0640db3a5e36fa625b0f17 ] hash: 0000008298-6f53e8ef03d9088888b4377b9caa53962ef71484fc93e92da376b530cead00d4 [Rolled back experiment. Nils Anders Danielsson **20110830095739 Ignore-this: 75f81bdf23a41a8a9c942b52ae750ace ] hash: 0000008258-0ef58a9283d5208a304ab0c380c304a351deb1052f167c3f2526fd221414d983 [Added from-just. Nils Anders Danielsson **20110830113530 Ignore-this: 1a6d2355e5380fdfefa65c0a8dfe0312 ] hash: 0000000505-8d2c6e50932c7dd7ad19daf5a006cb9b41d7d131b1911bb789b26919bdf9d4ae [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110830120608 Ignore-this: 3f5abf2beb747f022953b6d3294bb466 ] hash: 0000000432-b5a30acfcfabf94c4188875653bb935e31bcd19490b6595a088174e990a6677f [Removed Data.Context. Nils Anders Danielsson **20110905083545 Ignore-this: fad71e1914739c309194ee31289f34c1 ] hash: 0000005160-e46e26b36d221c68dd1f778c25e19718f871683ecaee87ded279388396f98a62 [Added case_return_of_. Nils Anders Danielsson **20110908064035 Ignore-this: 396da9594363f6a8fc8b0a0b2b283be + Based on an idea from Ulf Norell. ] hash: 0000001311-3e50847c5c7bef8907bb40e6b71a55d7086477833d661ca8b840f54cc136309b [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110908080852 Ignore-this: 43d24ed373086bf3310a55c209d86dec ] hash: 0000000315-5dbd848ab41afe50756de25e1a372118572e6c2127baca1679a43d787f9a169c [Removed HeterogeneousEquality. Added PropositionalEquality. Nils Anders Danielsson **20110908143146 Ignore-this: 326daf01ac88be06c4addea19988bd3e ] hash: 0000002249-73ea287dc3986520eba975bd34224fb946719a94e2fe97c73ce0538cd928d77c [Minor simplifications. Nils Anders Danielsson **20110909075133 Ignore-this: e803f1f1135bb020a1de9d71dbf81dc7 ] hash: 0000001140-e78fbd1b6c605bf33b65140ae718c705e31e33612d44ed83201d129c21a70201 [Removed forced and non-strict. Nils Anders Danielsson **20110911130948 Ignore-this: 7de8d7b1eff209dee011c5c3ec9496ad ] hash: 0000001281-03cbc7f89d230f71f5e5c8793789fc4952a5f9f6993a8bbe6f95849a2e339898 [Modified a comment. Nils Anders Danielsson **20110919152611 Ignore-this: e75c13481cc5c31eacad6ceb8fd892c0 ] hash: 0000000320-db5add24c41dcfba65d5d59c9ea71935a0e075ea60237776f3763580d0abc942 [Added header lines containing "The Agda standard library". Nils Anders Danielsson **20110919160432 Ignore-this: 86eb0dd2c01e8072979400cc9c158d4c ] hash: 0000013705-9cbb710338cb9560d255e78e3ba88755c662b9c36435226b5b5a67de6d0545a2 [Removed all occurrences of the --universe-polymorphism flag. Nils Anders Danielsson **20110924171117 Ignore-this: b5e6334c35c8352045c1fa5d9b428bb9 ] hash: 0000010581-a649b3ed3c71af650421f0f08b91d31a25f30f4ae4d9a4acec99a1bb38da0e3e [Cosmetic changes. Andrés Sicard-Ramírez **20110927134439 Ignore-this: 191d2505d5a99711930c6bc0da90cd51 ] hash: 0000001584-06d6e27bf6e6e85ad28e33e2d9c96b2148063c66a7df1e036016cbf4250a0da6 [Added ≡⇒ and EquationalReasoning._≡⟨_⟩_. Nils Anders Danielsson **20110929083202 Ignore-this: 44008e1aad87cb8e0cf653f1faf0246f ] hash: 0000000884-39b9592811956aa96fd128f37c550e96b5d56d0e45dd49264b9964dbfec2645d [Added Σ-assoc. Nils Anders Danielsson **20110930075818 Ignore-this: 380218becfc8ba7558b44662d60dcad0 ] hash: 0000001360-4dea54faec03263020a2f7e4901790751579d646dc38386b37bb0a115d1d0b37 [GenerateEverything now uses UTF8 when reading/writing Agda files. Nils Anders Danielsson **20111002171859 Ignore-this: fbbe7d96ebae1561f661d9b2359c8b33 ] hash: 0000000966-0de6c00fba6dd138971f4e9fc27887c06d50d16b480b83d0e3efbc52f16e35ae [Removed Relation.Binary.HeterogeneousEquality.Inspect. Nils Anders Danielsson **20111004170452 Ignore-this: 6f472f15a32c9464fca932ef50792a49 ] hash: 0000000582-8e56d52b136e5d3de00cbefcf344baa47a048cd877333c4b7f64cb7f995cbec5 [Added inspect on steroids. Deprecated the old inspect idiom. Nils Anders Danielsson **20111006134929 Ignore-this: 9773a83484aaf74102b95b202fcd30a0 + Inspect on steroids was invented by Ulf Norell. ] hash: 0000010018-b265fe2627cf4ba0be1ebe915ec617d64198a1628622e77cb1e28b7205cf9133 [Added a search tree invariant to the implementation of AVL trees. Nils Anders Danielsson **20111018101124 Ignore-this: f117a2c9e4f26105b5a3f312c46813d5 + I also made the module telescope slightly more restrictive: the ordering relation's underlying equality now has to be propositional equality. ] hash: 0000022377-ab457df7de59fd1a933230f4b819791cd5671d950fcd6ee46e5402be51c1bdaa [Made difference lists/vectors and AVL trees universe polymorphic. Nils Anders Danielsson **20111018101220 Ignore-this: fffcccb4e3380a53e872f57beb565238 ] hash: 0000007966-0780abf87f01f6dda0141d1a02ff2f7ebcb733e87ba4cef8a49a6401dd40ec90 [Added from-yes and from-no. Removed fromYes and fromYes-map-commute. Nils Anders Danielsson **20111104153050 Ignore-this: cdf864657efa94a45214bdfce0c32cd3 ] hash: 0000001733-d375f0f505267bb047bb57e66ae91a48f9503ce48b2383e9cde8ba19ce095d85 [Added ¬?. Nils Anders Danielsson **20111104153505 Ignore-this: 1323dfa7547f3041a34ce37718d45902 ] hash: 0000000353-bbd29ab994e9e995b0d3bc0d9b51567ee8d5dbfb449c2a3258a37d10596d53ab [Added Data.Nat.Primality. Nils Anders Danielsson **20111104153518 Ignore-this: 67edbc4fd105034acb5cda7cb21bf9f ] hash: 0000001187-2850d5179d0c5d68ea83c0f56f477aa6ce2cc1f38f3fadd71041a8a575429d30 [Added case_of_ and some examples (empty was suggested by Ulf Norell). Nils Anders Danielsson **20111111152031 Ignore-this: 6e4c328d0680c7a1529be2da173368a9 ] hash: 0000001465-5391b2a179a7353c0bfcc4d8ae9267604ef565c81fcfc276662f2aa65842323e [Added a README for the AVL tree module. Nils Anders Danielsson **20111111184550 Ignore-this: 56729b5cf67dbf50f4f7a78cbb6b26ab ] hash: 0000003365-a5eea6e8c63e1ddc3bd73c30e2e35e4cd14aee4b18e07f341a9373ac8f521a95 [More examples. Nils Anders Danielsson **20111111190533 Ignore-this: ef0d1d4977e4d96adf3643af5810ee61 ] hash: 0000000704-dde8e14e2d8e26ff0424b20af7deba5880d32145a7f4cf0168991bc7b05dd685 [Added _⊎-<-isStrictTotalOrder_ and _⊎-<-strictTotalOrder_. Nils Anders Danielsson **20111115154812 Ignore-this: 10f80dac81bdb48861a1728dfeb36af0 ] hash: 0000001505-8ff01bdf63a8ec8a3fe3dfb70f8d6837ea66a90fc30e7ad18330346c34ec23b7 [Minor simplification. Nils Anders Danielsson **20111119153035 Ignore-this: bc408c6b9832436fd31fc7e5695f988f ] hash: 0000000423-b8498718156a9cd145b7b011b429d41edb25f7f26af33a342da9c31e8f225c78 [Added some comments. Nils Anders Danielsson **20111119153054 Ignore-this: 5d95663087a4abe80a1eed9fd85e7484 ] hash: 0000000769-f5008e0a0695d72aa4566a7263c71fba95b32d09eec146c15ced47401a3d66bd [Merged README.txt and README.agda. Nils Anders Danielsson **20111205095916 Ignore-this: 876ca594753f9935dfa8c1175a244e5a ] hash: 0000001412-cc64428602fd12719d462b35983c6fd98a9d26eb1d9416ee99a80ae77f011916 [Added some missing combinators. Nils Anders Danielsson **20111206180546 Ignore-this: 3a641f8982beb62bd554f9f2ab03bfb4 ] hash: 0000014384-bb7d854b849c1529192ca2d127a16c8458325c8f283fcc2d13ff26977921c1b3 [Added strict total orders for characters and strings. Nils Anders Danielsson **20111206180633 Ignore-this: c6adb974d3f7c3b509061b6f1ebc4e00 ] hash: 0000001031-e18a79ae3a6dc443e0c8bb5039b3feaf56e53d59dc5ea2317e4ab68ca6a3047b [Made 'x' ≟ 'x' compute properly by replacing a postulate with trustMe. Nils Anders Danielsson **20111206173552 Ignore-this: 3bd1c2246465c442ec4772ba0ccd9199 ] hash: 0000000462-62ae0ee9d6b1d5128a6423c8d25983af0a37cbcf06a72a0dbdfb5b1301c3bf96