[Initial bag example, illustrates problem. Nils Anders Danielsson **20060518025226] [Implemented decRel (and changed its interface). Nils Anders Danielsson **20060518072034] [Added Leibniz' equality. Nils Anders Danielsson **20060518081135] [Isolated problem by defining Traverse view. Nils Anders Danielsson **20060518081206] [Illustrated another problem. Nils Anders Danielsson **20060518081735] [Added datoids. Changed Bag interface and most of its implementation. Nils Anders Danielsson **20060518104617] [Introduced a datatype for the bag datatype, to prepare for later invariants. Nils Anders Danielsson **20060522025736] [Added a module for positive numbers. Nils Anders Danielsson **20060522052136] [Started using positive instead of natural numbers in internal bag type. Nils Anders Danielsson **20060522052815 + We still have one more invariant (no duplicates allowed), so this does not make our case study less general. ] [Added $. Nils Anders Danielsson **20060522055857] [Added Unit. Nils Anders Danielsson **20060522055909] [Added decRel''. Nils Anders Danielsson **20060522055930] [Added map and member. Nils Anders Danielsson **20060522055945] [Removed unnecessary implicit parameters (necessary in early Agda2 version). Nils Anders Danielsson **20060522060853] [Added id. Nils Anders Danielsson **20060522063746] [Removed decRel'' again (stupid function, we already had rel''). Nils Anders Danielsson **20060522063807] [Changed definition of member; hidden argument impossible to infer. Nils Anders Danielsson **20060522081612] [Fixed small bug; hidden argument not inferred. Nils Anders Danielsson **20060522081734] [Renamed refl to leibnizRefl. Nils Anders Danielsson **20060523005725] [Added contrapositive. Nils Anders Danielsson **20060523011209] [Removed SubstDecEq. Replaced with DecidableEquiv in Datoid. Nils Anders Danielsson **20060523011905 + Reason: We can not expect arbitrary ADTs to have substitutive equalities. The bags are one example. ] [Added datoidRel. Nils Anders Danielsson **20060523012051] [Added refl, sym and trans, plus lifted variants for datoids. Nils Anders Danielsson **20060523012152] [Added notDistribOut and notDistribIn. Nils Anders Danielsson **20060523025310] [Added memberPreservesEq. Nils Anders Danielsson **20060523025401] [Added NoDuplicates. Nils Anders Danielsson **20060523025429] [Removed need for stupid pattern matching by changing definition of datoidRel. Nils Anders Danielsson **20060523041203] [Introduced bag invariant. Nils Anders Danielsson **20060523055106 + Also made more things abstract. ] [Added T and T'. Nils Anders Danielsson **20060523075116] [Added <-> and some helpers. Nils Anders Danielsson **20060523075156] [Moved Eq, made impl abstract, changed impl, added more helpers. Nils Anders Danielsson **20060523075506] [Proved that boolean functions can be turned into decidable relations. Nils Anders Danielsson **20060523075638] [Added absurdElim. Nils Anders Danielsson **20060523090501] [Added natDatoid and posDatoid. Nils Anders Danielsson **20060523095651] [Added && and andT. Nils Anders Danielsson **20060523113208] [Added pairEquiv. Nils Anders Danielsson **20060523113413] [Added pairDatoid. Nils Anders Danielsson **20060523113650] [Added datoidDecRel. Nils Anders Danielsson **20060523113755] [Added delete and Permutation. Nils Anders Danielsson **20060523113842] [Defined BagEquiv. Nils Anders Danielsson **20060523120918] [Fixed problems related to unsolved constraints. Nils Anders Danielsson **20060523120959] [Added Maybe. Nils Anders Danielsson **20060523123735] [Added pred. Nils Anders Danielsson **20060523123754] [Added Pi and apply. Nils Anders Danielsson **20060523135322] [Added noCopies. Nils Anders Danielsson **20060523142455] [Changed to a simpler (proof-wise) definition of perm. Proved some lemmas. Nils Anders Danielsson **20060524001100] [Added Respects and subst. Nils Anders Danielsson **20060524014326] [Traverse and run are no longer abstract. Nils Anders Danielsson **20060524014600] [Added some postulated lemmas about insertion. Nils Anders Danielsson **20060524040423] [Changed interface of bagElim (predicate has to respect bag equality). Nils Anders Danielsson **20060524040808 + Defined bagElim in terms of traverse and traverseTraverses. + Defined traverse. + Started on traverseTraverses, which is tricky since positive numbers are abstract. (Maybe positive numbers should have been our case study...) + Made some helper functions local. ] [Added headlines. Nils Anders Danielsson **20060524044353] [Postulated some respect and equality preservation lemmas. Nils Anders Danielsson **20060524055212] [Added sketch indicating why it's messy to prove traverseTraverses. Nils Anders Danielsson **20060524055431 + It might be easier if we had some sort of congruence types and/or rewrite rules for ADTs. ] [added listDatoid Hiroyuki Ozaki **20060523055640] [merged listDatoid and Permutation patches Hiroyuki Ozaki **20060524042634] [add parser combinators Hiroyuki Ozaki **20060524061217] [Resolved conflict arising from Hiroyuki's patches. Nils Anders Danielsson **20060620142726] [Inserted some ?s to make Hiroyuki's code type check. Nils Anders Danielsson **20060620143717 + The code failed to type check since I had changed the interface of the bag ADT. ]