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