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