[TAG 0.1 Nils Anders Danielsson **20090423152846 Ignore-this: 8ba8b251333b344453895f42da937e75 ] < [Preparation for the first release. Nils Anders Danielsson **20090423152613 Ignore-this: f0ddfa6d9ed30213f3f80d76603fd13 ] [Made more things boring. Nils Anders Danielsson **20090423142709 Ignore-this: 1a58dfa00484041815f964e8987c7e57 ] [The Everything module is now automatically generated. Nils Anders Danielsson **20090423142412 Ignore-this: fccd6b7b36fc47f57d07927b8a05c39c + Except for one line which is used to work around a bug in Agda 2.2.2. ] [Expanded the README considerably. Nils Anders Danielsson **20090423141603 Ignore-this: 95825bd051ceda9cbf0317996b0d5bea + Moved some content from the Agda Wiki into the README to keep things in one place. ] [Removed Algebra.RingSolver.Examples. Nils Anders Danielsson **20090423133535 Ignore-this: 263bdc02f14abeab76134dfdb433dd04 ] [Added _×₀₁_, _×₁₀_ and _×₁₁_. Nils Anders Danielsson **20090420165420 Ignore-this: 59e9cd9419110e7aa1dc6859999262fc ] [Made some functions lazier. Nils Anders Danielsson **20090420124353 Ignore-this: 1e058e09a218610a99746b7a7213eb0b ] [Updated preferences after conversion to darcs 2 format. Nils Anders Danielsson **20090416185210 Ignore-this: 1fe888efce4c4bed6e42e19b8c7c84c6 ] [Added code intended to ease development of reflection-based "tactics". Nils Anders Danielsson **20090415142123 Ignore-this: f1bc11041b83ad19e8fb1a921a0fc91e ] [Added solve, a nicer interface to the ring solver. Nils Anders Danielsson **20090415122544 Ignore-this: 4fd57040e1b376dbdfd663b02f248984 + I took the idea for solve from Ulf Norell. ] [Added Eqʰ. Nils Anders Danielsson **20090415113127 Ignore-this: dea79d4b3d6410727dbe1c7badc20de4 ] [Improved a comment. Nils Anders Danielsson **20090415113120 Ignore-this: 1ee073d8ef58895b7baf5852cb41b19a ] [Removed a workaround which is no longer necessary. Nils Anders Danielsson **20090414120031 Ignore-this: 6dfa782776ef12ec0e02435c126371a7 ] [Exported _≡⟨_⟩_ and ≡-byDef from ≅-Reasoning. Nils Anders Danielsson **20090414114003 Ignore-this: e5878cabb523d98e036fec15512c87a0 ] [Renamed Reasoning to ≅-Reasoning (in analogy with ≡-Reasoning). Nils Anders Danielsson **20090414113927 Ignore-this: 6f1be5b0e4d988d6180ba4511ad65549 ] [Renamed some local definitions. Nils Anders Danielsson **20090414113830 Ignore-this: ce753d471509f777063eae2b34bd8cae ] [Updated a comment. Nils Anders Danielsson **20090414112402 Ignore-this: 607941a9583dc7a3c129617939c6f125 ] [Added Any and All. Nils Anders Danielsson **20090403110025 Ignore-this: 405c9cb76a15f978a6dc043513922e68 ] [Proved some lemmas related to non-empty lists. Nils Anders Danielsson **20090403103757 Ignore-this: 6ac46fe4513f9b65adabecfd2e6d49bf ] [Proved some lemmas related to _∈_. Nils Anders Danielsson **20090403103709 Ignore-this: b3eceee3c1e4dbfba61e8789db35966a ] [Renamed _++_ to _⁺++⁺_. Added _⁺++_ and _++⁺_. Nils Anders Danielsson **20090402095849 Ignore-this: ec73be4f934228614aa7841b98d81ab ] [Added more examples. Nils Anders Danielsson **20090402095750 Ignore-this: 3f1d47b1df2c31b7421d7c34134e92f7 ] [Improved the evaluation behaviour of a function. Nils Anders Danielsson **20090402094501 Ignore-this: bc0cd5a2b7597cac115426adb050aafb ] [Proved b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂. Nils Anders Danielsson **20090330204507 Ignore-this: 3abe2459125e09abf8b44e8b0dc35777 ] [Renamed contravariant to contraposition. Nils Anders Danielsson **20090327105237 Ignore-this: 76e83862bf1461cba042b3fa3af8ff21 ] [Generalised [_,_]. Nils Anders Danielsson **20090327092702 Ignore-this: 44361f1121e6196b7a63b5c413f367d7 ] [Proved some properties relating _≡_, _≢_ and not. Nils Anders Danielsson **20090327010036 Ignore-this: bd866f88994c01d70d91f4f91ac7e19b ] [Added intersperse. Nils Anders Danielsson **20090326130702 Ignore-this: 7fb6fd3d9fe4e461cb2d6314f6ef5202 ] [Added _∷ʳ_. Nils Anders Danielsson **20090326114739 Ignore-this: f0ebe49f9408423d7c70e53fee6e9651 ] [Added _∶₁_. Nils Anders Danielsson **20090324165718 Ignore-this: 9e308196f6073832f4d5fa6c541dfbe8 ] [Added foldr and foldl. Nils Anders Danielsson **20090323165701 Ignore-this: b41fa695946748e2a4194bb26cfba6cf ] [Added a productivity checker workaround. Nils Anders Danielsson **20090317014259 Ignore-this: 5762b761b4f1104fc397273881fe1a34 ] [Added if₁_then_else. Nils Anders Danielsson **20090316124233 Ignore-this: 7452b9f0a6ad0fe4f5ea09287d46c6fa ] [Added map₀₁, map₁₀ and map₁₁. Nils Anders Danielsson **20090315004251 Ignore-this: 4553d939ec84a8c0e6afab18af5bc3ca ] [Added ∃₀₁, ∃₁₀ and ∃₁₁. Nils Anders Danielsson **20090315004043 Ignore-this: a4965307ddcf27cbf65fb1ef1b81b9b6 ] [Renamed ringSolver to RingSolver and xor-ringSolver to XorRingSolver. Nils Anders Danielsson **20090313174543 Ignore-this: d1ce29c8304a7bd2889877bd25d61c9f ] [Many minor simplifications (inferable record fields can now be omitted). Nils Anders Danielsson **20090309181918 Ignore-this: 6ad1b0d403161675e89755e5e31073fe ] [Added map. Nils Anders Danielsson **20090308121035 Ignore-this: b350f17604e79aa302212643d9b826de ] [Minor simplifications. Nils Anders Danielsson **20090308120938 Ignore-this: ff77149e1f11efaf0565641e06d30049 ] [Added Decidable Total Order of Integer Liang-Ting Chen **20090308054918] [Added Any and All. Nils Anders Danielsson **20090305201914 Ignore-this: 9210ebd0b0f0ce3b0a2b947156bcbb2d ] [Added Any and All. Nils Anders Danielsson **20090305184700 Ignore-this: 6a57d24894de20ce6612a945686be717 ] [Renamed -- to -‿. Nils Anders Danielsson **20090304191624 Ignore-this: 9c5b309b6e224b59acd17402ac53a0fc ] [Added right-identity-unique. Nils Anders Danielsson **20090304122937 Ignore-this: 4653d8b6e76fcafd7a6f236199772212 ] [Simplification. Nils Anders Danielsson **20090304122846 Ignore-this: 2a529ac1a5ee9a3f720c15bc43264f63 ] [Proved that identity elements are unique. Nils Anders Danielsson **20090304121533 Ignore-this: be419883bd902e1bdfc2a892184dcc3b ] [Fixed more bugs due to constructors not being in scope. Nils Anders Danielsson **20090228191541 Ignore-this: b867b1f1d4425025198c8c3861e8b7d6 + These bugs were detected by Agda, which now checks for (certain instances of) this problem. ] [Added ¬-drop-Dec. Nils Anders Danielsson **20090227105622 Ignore-this: 36f72b7e0f4397f16db49a7aa0f8d6b2 ] [Updated code to reflect changes in Agda. Nils Anders Danielsson **20090226004414 Ignore-this: c358047befb72e634a4fbda9aca0130f ] [Proved that a number of properties are preserved by flip₁. Nils Anders Danielsson **20090219195737 Ignore-this: c6a979238c229c43247dad9095eccbfe ] [Added the partiality monad. Nils Anders Danielsson **20090219190640 Ignore-this: 381e42dc3860de43a3accb57e151cf79 ] [Added monadT. Nils Anders Danielsson **20090219185610 Ignore-this: 8561285e6a390f5242c10e400e078a58 ] [Fixed a bug: A constructor was not in scope, so a pattern always matched. Nils Anders Danielsson **20090219181609 Ignore-this: 61b60b73495f0e7ef6af827e68568e0e ] [Added _[_]≔_. Nils Anders Danielsson **20090219181432 Ignore-this: d694fdfb46e73bce662cefcf5cd0300d ] [Added lookup-natural. Nils Anders Danielsson **20090211204640 Ignore-this: cbac62a371b283aef344526e00755e03 ] [Added reverse. Nils Anders Danielsson **20090211002357 Ignore-this: 2e9f006cee0bf6b98bb80ebcdfca2d60 ] [Added concat and monad. Nils Anders Danielsson **20090211001744 Ignore-this: 913b74219b17f7c636599c74c77cd93c ] [Added isInj₁/isInj₂. Removed inj₁s/inj₂s. Nils Anders Danielsson **20090210231940 Ignore-this: c14254e1921c27861411957ac344f20d + Use gfilter isInj₁/gfilter isInj₂ instead of the removed functions. ] [Added head and tail. Nils Anders Danielsson **20090210225716 Ignore-this: f51190033cf86c83d5adeb1a4b5c5c69 ] [Added fromList and toList. Nils Anders Danielsson **20090210225449 Ignore-this: 21e9a361b7ab776343229c661447e028 ] [Updated code to reflect changes in Data.Vec.Equality. Nils Anders Danielsson **20090206140900 Ignore-this: 22c5b1425d51cac732f316754381ce5e ] [Minor changes. Nils Anders Danielsson **20090206140835 Ignore-this: b137522cd9da68537c42869dadc1f529 ] [Added Liang-Ting Chen as a copyright holder. Nils Anders Danielsson **20090206134835 Ignore-this: d6d01886663676a957cd86f339e5c93b ] [Updated the copyright year range. Nils Anders Danielsson **20090206134809 Ignore-this: 402803aebe2dafad98507f3a63932d54 ] [Data.Vec.Equality_with_Setoid_DecSetoid Liang-Ting Chen **20090206120253] [Vector_Equality_With_Setoid_DecSetoid Liang-Ting Chen **20090205151918] [Added gmap-cong. Nils Anders Danielsson **20090204201347 Ignore-this: bdf898f389efc292de2fd9edafcd5810 ] [Added gmap-id and gmap-∘. Nils Anders Danielsson **20090204195452 Ignore-this: 9f18550c51153c482f08aea52f36390e ] [Added a list monoid. Nils Anders Danielsson **20090204193230 Ignore-this: a44058905bc5cb3fbdd3464500fb8b56 ] [Added gmap-◅◅ and fold-◅◅. Nils Anders Danielsson **20090204190526 Ignore-this: deb4c90d8bc3c62e493026d99c436233 ] [Added Data.Star.Properties. Moved some properties from Data.Star. Nils Anders Danielsson **20090204185414 Ignore-this: 6faaf1626f95e0e8fe19f3afaa0bf6f0 ] [Added fromMaybe. Nils Anders Danielsson **20090204180950 Ignore-this: 4414606052af24a153e590eb5c20f8b0 ] [Added fromColist. Nils Anders Danielsson **20090130135348 Ignore-this: b729a73dc150b0692eee2e5bb519d184 ] [Added length. Nils Anders Danielsson **20090130135334 Ignore-this: be970a2761d72fb2775b1e37f10cdcf1 ] [Changed the implementation of _++_. Nils Anders Danielsson **20090127172847 Ignore-this: 98fd4018eb9f88e7634e26e557a33402 + The previous implementation traversed the second argument (twice). ] [Added concat. Nils Anders Danielsson **20090127172648 Ignore-this: e289dc41e53d3602560442b977cddd2e ] [Changed the reduction behaviour of fromVec. Nils Anders Danielsson **20090127170622 Ignore-this: d0fb0fb2b616792935115e8fb0e594c8 ] [Added documentation. Nils Anders Danielsson **20090127111413 Ignore-this: 71c7af72a56f218ad0513ea7a289dd07 ] [Added replicate. Nils Anders Danielsson **20090127111046 Ignore-this: 7ccb3749b5d424dd68f91b26e806f99c ] [Added Coℕ, Cofin and Covec. Nils Anders Danielsson **20090127110946 Ignore-this: a36975087fe0229e7e7b582e160c1e19 ] [Added mapM and mapM′. Nils Anders Danielsson **20090124220147] [Added _∘′_, a non-dependent variant of _∘_. Nils Anders Danielsson **20090124214618 + The function _∘′_ can be useful when the hidden arguments of _∘_ cannot be inferred. ] [Added head, tail, zipWith, drop, repeat and _⋎_. Nils Anders Danielsson **20090124214002] [Fixed bug in _++_. Nils Anders Danielsson **20090124001307 + This bug was discovered when I implemented a more well-typed variant of _++_ for covectors. ] [Made some names involved in corecursive definitions more descriptive. Nils Anders Danielsson **20090123140324 + Following Noam Zeilberger. ] [Made some private definitions public. Nils Anders Danielsson **20090122232226] [Increased code reuse. Nils Anders Danielsson **20090122160901] [Added Fin′. Nils Anders Danielsson **20090120183151] [Added ¬∀⟶∃¬ and ¬∀⟶∃¬-smallest. Nils Anders Danielsson **20090120172256] [Added inject and inject-lemma. Nils Anders Danielsson **20090120172239] [Generalised ≡↝. Nils Anders Danielsson **20090120164141] [Improved a comment. Nils Anders Danielsson **20090120143458] [Generalised the type of call/cc. Nils Anders Danielsson **20090120143450] [Added ≤⇒pred≤. Nils Anders Danielsson **20090120143235] [Added inject≤-lemma. Nils Anders Danielsson **20090120010322] [Added sequence. Nils Anders Danielsson **20090119194853] [Added sequence, a generalisation of ¬¬-pull. Nils Anders Danielsson **20090119193137] [Moved parts of Relation.Nullary to Relation.Nullary.(Negation|Decidable). Nils Anders Danielsson **20090119183235] [Added an induction scheme based on the fact ∀ (i : Fin n) → toℕ i < n. Nils Anders Danielsson **20090119161533] [Added take-⊑. Nils Anders Danielsson **20090119141716] [Made a type signature shorter but (perhaps) harder to understand. Nils Anders Danielsson **20090119141635] [Proved that (Colist A, _≈_, _⊑_) is a poset. Nils Anders Danielsson **20090119113009] [Renamed _PrefixOf_ to _⊑_. Nils Anders Danielsson **20090119112925] [Removed a pointless function. Nils Anders Danielsson **20090119110559] [Updated code to reflect changes in Agda. Nils Anders Danielsson **20090116174042] [Fixed bug in take (both for streams and for colists). Nils Anders Danielsson **20090115222216 + This bug would not have been introduced if the types of the take functions had been more precise. Now the types are more precise. ] [Removed many prefixes (renamed ≡-refl to refl, for instance). Nils Anders Danielsson **20090114225114 + Use the module system to avoid ambiguities. ] [Generalised the type of <_,_>. Nils Anders Danielsson **20090114214939 + Also removed some functions which were simple instances of others, and renamed some functions. ] [Added streams. Nils Anders Danielsson **20090113234543] [Defined a coinductive wrapper for the IO monad. Nils Anders Danielsson **20090113233111 + To make it possible to write "infinite" IO computations without turning off the termination checker. ] [Found a seemingly nicer way to define types with coinductive components. Nils Anders Danielsson **20090113232129 + Defined a type ∞ which can be used to mark a recursive argument as being coinductive. + Modified Data.Colist to use this approach, and added a number of definitions. ] [Moved a type tightly coupled to the Haskell FFI to Foreign.Haskell. Nils Anders Danielsson **20090113231247] [Added a comment. Nils Anders Danielsson **20090113205743] [Lowered the precedence of _⇔_ to make it bind weaker than _≡_. Nils Anders Danielsson **20090110130603] [Fixed bug: Haskell does not use λ and → (by default). Nils Anders Danielsson **20090108015904] [Generalised the type of ∃₂. Nils Anders Danielsson **20090105204512] [Switched from (forall, ->, \) to (∀, →, λ). Nils Anders Danielsson **20090104201731] [Added Data.Empty1. Nils Anders Danielsson **20081219162149] [Added Data.Unit1. Nils Anders Danielsson **20081219162022] [Replaced → with ⟶, because → has become a reserved character. Nils Anders Danielsson **20081217150737] [Switched to the most general variant of _∘_. Nils Anders Danielsson **20081216001732 + This variant is not quite a drop-in replacement for the previous one (as exemplified by this patch), because its type can make hidden arguments more difficult to infer. However, I now think that the limits of the limited variant are more annoying than the problems with the general one. + Removed _∘′_. ] [Defined join. Nils Anders Danielsson **20081215213157] [The script now produces links to /highlighted/ source code. Nils Anders Danielsson **20081210165618] [Improved header. Nils Anders Danielsson **20081202101544] [The program now counts the number of occurrences of every character. Nils Anders Danielsson **20081201070521] [Improved some headers. Nils Anders Danielsson **20081201064702] [added types signatures to some lambdas ulfn@cs.chalmers.se**20081128102025] [Switched to a different implementation of fromBits. Nils Anders Danielsson **20081118103956] [Added Patrik as a copyright holder. Nils Anders Danielsson **20081114183823] [A two-arg cong added. patrikj@chalmers.se**20081114123044] [Made the Set argument to excluded-middle hidden. Nils Anders Danielsson **20081107181515] [Removed reductio-ad-absurdum-⊎. Nils Anders Danielsson **20081107181409] [Added call/cc. Nils Anders Danielsson **20081107163007] [Commented out some tests because they take a long time to type check. Nils Anders Danielsson **20081106125247] [Improved the header text. Nils Anders Danielsson **20081105143715] [Simplified the implementation of showDigit. Nils Anders Danielsson **20081105143329] [Improved a comment. Nils Anders Danielsson **20081104213556] [Proved m ≤ n -> m ≤ k + n. Nils Anders Danielsson **20081104185135] [Renamed some things from foo-¬¬ to ¬¬-foo. Nils Anders Danielsson **20081103102332] [Proved that double-negation forms a monad. Nils Anders Danielsson **20081103101842] [A module containing the sizes used by sized types. Nils Anders Danielsson **20081028175813] [Removed many functions which can be replaced by \() or \{}. Nils Anders Danielsson **20081028142414] [Added non-empty lists. Nils Anders Danielsson **20081027193700] [Changed the precedence of _∣_ from 5 to 3. Nils Anders Danielsson **20081027175651 + Because I want _∣_ to bind weaker than _⊛_ and _<$>_. + This also matches the precedence of (<|>) in the Haskell library Control.Applicative. ] [Administrative tweaks. Nils Anders Danielsson **20081014122431] [Delimited continuation monad and monad transformer. Dan Doel **20081014121949] [Removed use of BUILTIN IO, which is no longer necessary. Nils Anders Danielsson **20081007142856] [Added idM, _∘M_ and constM. Nils Anders Danielsson **20080924174347] [Added pred-mono. Nils Anders Danielsson **20080904165331] [Added some functions and a module related to non-indexed state monads. Nils Anders Danielsson **20080902182459] [Added sequence and mapM. Nils Anders Danielsson **20080902182253] [Proved that many properties which hold for _∼_ also hold for _∼_ on₁ f. Nils Anders Danielsson **20080901000613] [Added ×-compare, _×-isStrictTotalOrder_ and _×-strictTotalOrder_. Nils Anders Danielsson **20080831214253] [Added some tests. Nils Anders Danielsson **20080831142924] [Added zipWith and zip. Nils Anders Danielsson **20080831135728] [Added pred and downFrom. Nils Anders Danielsson **20080831135041] [Added _<_ and proved that (Bin, _≡_, _<_) is a strict total order. Nils Anders Danielsson **20080831132916] [Added _<_ and proved that (Fin n, _≡_, _<_) is a strict total order. Nils Anders Danielsson **20080831132847 + Also moved some definitions from Data.Fin to Data.Fin.Props. ] [Added []≢∷. Nils Anders Danielsson **20080831132737] [Proved that (ℕ, _≡_, _<_) is a strict total order. Nils Anders Danielsson **20080831102058] [Dropped the ℕ- prefix from many names. Nils Anders Danielsson **20080831101549] [Noted that strict total orders have a /decidable/ underlying equality. Nils Anders Danielsson **20080831095740] [Cosmetic changes. Nils Anders Danielsson **20080830075943] [Added an implementation of finite sets. Nils Anders Danielsson **20080829165040] [Added values indexed on keys to Data.AVL. Nils Anders Danielsson **20080829155904 + By using this new interface I could also remove a hack from the implementation of Data.AVL.IndexedMap. ] [Added an implementation of finite maps with indexed keys/values. Nils Anders Danielsson **20080829143644] [Made some comments more precise. Nils Anders Danielsson **20080829011323] [Made the type of lookup more informative. Nils Anders Danielsson **20080829010956] [Added _∈?_. Nils Anders Danielsson **20080828220444] [Generalised maybeToBool. Nils Anders Danielsson **20080828220212] [Added delete, headTail and initLast. Nils Anders Danielsson **20080828151750] [Added "difference vectors". Nils Anders Danielsson **20080828151408] [Added lift, take and drop. Nils Anders Danielsson **20080828150303] [Removed the value component from the AVL trees. Nils Anders Danielsson **20080828083859] [Added an implementation of AVL trees. Nils Anders Danielsson **20080827223116] [Added some lemmas relating length to other list functions. Nils Anders Danielsson **20080821001716] [Cosmetic changes. Nils Anders Danielsson **20080818165908] [Renamed [_] to List and singleton to [_]. Nils Anders Danielsson **20080818165846] [Mostly cosmetic changes. Nils Anders Danielsson **20080817134323] [A representation of directed acyclic multigraphs. Nils Anders Danielsson **20080815165401] [Added Data.Bool.Show. Nils Anders Danielsson **20080815145202] [Sets in injective correspondence with Fin n have decidable equality. Nils Anders Danielsson **20080815133416] [Added representations of injections and left inverses. Nils Anders Danielsson **20080815133325] [Added _∈_. Nils Anders Danielsson **20080814211150] [Added Set1 variants for some existing Set-based code. Nils Anders Danielsson **20080814123846] [Added decSetoid. Nils Anders Danielsson **20080813125534] [Added ∃₂. Nils Anders Danielsson **20080813021619] [Added nℕ-ℕi≤n. Nils Anders Danielsson **20080813021554] [Renamed _++₁_ to _++_ and replicate₁ to replicate. Nils Anders Danielsson **20080812132127] [Added length. Nils Anders Danielsson **20080812132045] [Added a bunch of Fin-related functions. Renamed others. Nils Anders Danielsson **20080811204927 + Added fromℕ≤, #_, inject₁, fold, _-_, _ℕ-_, pred and reverse. ] [Added gfilter. Nils Anders Danielsson **20080811185129 + Removed catMaybes, since catMaybes = gfilter id. ] [Added ≤pred⇒≤. Nils Anders Danielsson **20080808151157] [Added catMaybes. Nils Anders Danielsson **20080807181235] [Added ≡₁₀-cong. Nils Anders Danielsson **20080804153722] [Added _+⋎_ and _⋎_. Nils Anders Danielsson **20080731225214] [Added _>>=_ and _⊛_. Nils Anders Danielsson **20080731225132] [Added putStr. Nils Anders Danielsson **20080730144554] [Improved formatting. Nils Anders Danielsson **20080730144533] [removed duplicate open public ulfn@cs.chalmers.se**20080730093253] [Added MaybeFunctor. Nils Anders Danielsson **20080726223637] [Code for converting Vec₁ n A -> B to and from n-ary functions. Nils Anders Danielsson **20080724184111] [Added map, map₁₀ and lookup. Nils Anders Danielsson **20080724183801] [Code for converting Vec n A -> B to and from n-ary functions. Nils Anders Danielsson **20080724162025] [Added allFin. Nils Anders Danielsson **20080724022554] [Replaced many occurrences of • with ∙. Nils Anders Danielsson **20080723011636 + I.e., replaced bullets with bullet operators (when appropriate). With the new Agda input method it is easier to write ∙ than • (at least for me). + Also replaced ○ (white circle) with ∘ (ring operator), but this did not affect public interfaces. ] [Added _:-_. Nils Anders Danielsson **20080723005720] [Changed the types and definitions of take and drop. Nils Anders Danielsson **20080721214625 + I think the new definitions are more usable. ] [Proved that (m ∸ n) ⊓ (n ∸ m) ≡ 0. Nils Anders Danielsson **20080719210909] [Added const₁. Nils Anders Danielsson **20080719082925] [Added _++_. Nils Anders Danielsson **20080719082849] [Added ≡↝. Nils Anders Danielsson **20080715183229] [Renamed LogicalRelation to _↝_. Nils Anders Danielsson **20080715183209] [Added a universe of proposition functors. Nils Anders Danielsson **20080715182637] [Added Always-isEquivalence. Nils Anders Danielsson **20080715180649] [Added more documentation for the inspect idiom. Nils Anders Danielsson **20080715162411] [Program which outputs all non-ASCII characters used by the library code. Nils Anders Danielsson **20080715161610] [Fixed a mistake in the previous enlargement of gcd's domain. Nils Anders Danielsson **20080708155048] [Added some lemmas about ¬_. Nils Anders Danielsson **20080624133806] [Added ,_. Nils Anders Danielsson **20080619182931] [Named many constructor arguments. Nils Anders Danielsson **20080618141949 + Hopefully this will make case-split slightly more useful. ] [Enlarged the domain of putStrLn. Nils Anders Danielsson **20080618134209] [Added toCostring. Nils Anders Danielsson **20080618134023] [Added fromList and take. Nils Anders Danielsson **20080618134017] [Moved Costring to Data.String. Nils Anders Danielsson **20080617172002] [Moved the one-constructor unit type to Data.Unit. Nils Anders Danielsson **20080617171430] [added COMPILED_TYPE pragmas and fixed incorrect types for IO functions ulfn@cs.chalmers.se**20080617151131] [update to conform to new COMPILED_DATA directive ulfn@cs.chalmers.se**20080617144841] [Added an equality test and some conversions. Nils Anders Danielsson **20080617141202] [Added a module for signs. Nils Anders Danielsson **20080617132943] [Renamed ℕ-≟ to ≟. Nils Anders Danielsson **20080617122816] [Generalised some types. Nils Anders Danielsson **20080617122321] [Made the integers concrete. Nils Anders Danielsson **20080617120202] [Added a BUILTIN pragma for IO. Nils Anders Danielsson **20080616151853 + It is now checked that main has type IO a for some a. ] [Reformatted Everything to match the format expected by GenerateDocs.hs. Nils Anders Danielsson **20080616141602] [Removed some outdated BUILTIN pragmas. Nils Anders Danielsson **20080616135030] [Renamed Σ₀ to ∃. Added ∄. Nils Anders Danielsson **20080614232452] [Added simple support for IO. Nils Anders Danielsson **20080613144814] [Added coinductive lists. Nils Anders Danielsson **20080613144124] [Made MAlonzo boring. Nils Anders Danielsson **20080613143852] [Removed Data.Unit.Core. Nils Anders Danielsson **20080613142025] [Removed Data.Sum.Core. Also removed inj₁≢inj₂. Nils Anders Danielsson **20080611170450] [Renamed fz to zero and fs to suc. Nils Anders Danielsson **20080605115344] [Added _∶_. Nils Anders Danielsson **20080605114226] [Reduced the number of dependencies for Data.Vec and Data.Fin. Nils Anders Danielsson **20080605100138 + Ulf informed me of how one can define the efficient reverse for vectors, with the expected type signature, without any proof code. ] [Strengthened prop-toℕ-≤. Nils Anders Danielsson **20080605094557] [Enlarged the domain of gcd. Nils Anders Danielsson **20080604222409] [removed uses of as-patterns ulfn@cs.chalmers.se**20080604155815] [update to avoid shadowing module names ulfn@cs.chalmers.se**20080604155740] [Generalised zip-Σ. Nils Anders Danielsson **20080522125625] [Add map-\Sigma to Data.Product (dependant version of map-\times) Samuel Bronson **20080522012155] [Added _≥′_ and _>′_. scm@iis.sinica.edu.tw**20080521144419] [Added _⟶⟨_⟩_. Nils Anders Danielsson **20080520134819] [Added Samuel Bronson to the list of copyright holders. Nils Anders Danielsson **20080518151821] [Added Samuel's comment to Data.Unit.Core as well. Nils Anders Danielsson **20080518150244] [Alleviate confusion regarding the name of the unit type Samuel Bronson **20080513181522 The \top symbol sometimes looks a lot like a T, so I added comments to Data.Unit pointing out that the type exported from there is named with a \top, not a T. ] [Improved formatting. Nils Anders Danielsson **20080515211656] [Added _⇔_. Nils Anders Danielsson **20080515210056] [Added _⊇_. Nils Anders Danielsson **20080515194103] [Turned splitAt and group into views. Added a view for init and last. Nils Anders Danielsson **20080514084000] [Added _∷ʳ_. Nils Anders Danielsson **20080514083831] [Added head and tail. Nils Anders Danielsson **20080513181149] [Fixed bug. (Thanks to naesten for reporting it.) Nils Anders Danielsson **20080509002258] [Made e an explicit argument in fold-fusion. scm@iis.sinica.edu.tw**20080507105106] [Extending Data.List and Data.List Properties. scm@iis.sinica.edu.tw**20080507083445 + New functions in Data.List: concatMap, and, or, any, all, product, scanr, scanl, take, drop, splitAt, takeWhile, dropWhile, span, break, inits, tails, and partition. + New properties in Data.List.Properties: ∷-injective, take++drop, splitAt-defn, takeWhile++dropWhile, span-def, partition-defn, scanr-defn, and scanl-defn. + Rearranged Data.List according to the way Hugs arranges Data/List.hs. ] [Removed the "flexible" variants of preorder reasoning. Nils Anders Danielsson **20080502133656] [Removed an empty directory. Nils Anders Danielsson **20080502003158] [Added more functions influenced by set theory. Renamed ⟶ to ⊆. Nils Anders Danielsson **20080502003126] [Removed Data.Bool.Core. Added Relation.Nullary.Core instead. Nils Anders Danielsson **20080501225907 + Bool is (perhaps) more likely to be used by beginners, so I want to avoid complication in that module. ] [Added Relation.Binary.Props.DecTotalOrder. Nils Anders Danielsson **20080501131118] [Moved the Logic.Induction hierarchy to Induction. Nils Anders Danielsson **20080501124527] [Improved formatting. Nils Anders Danielsson **20080430221127] [Added _¬-⊎_. Nils Anders Danielsson **20080430221055] [Removed Logic. Nils Anders Danielsson **20080430220532 + Removed ∃. Use Data.Product.Σ instead. + Moved _≡_ to Relation.Binary.PropositionalEquality. + Moved ⊥ to Data.Empty. + Moved ¬_ to Relation.Nullary. ] [Added strict total orders. Nils Anders Danielsson **20080430205114] [Renamed the constructors of the Tri data type. Nils Anders Danielsson **20080430205005] [Renamed Preorder.refl to reflexive. Added Preorder.refl. Nils Anders Danielsson **20080430201642] [Added a module for "strict partial order reasoning". Nils Anders Danielsson **20080430190653] [Extended an export list. Nils Anders Danielsson **20080430171958] [Added maybe and maybe₀₁. Nils Anders Danielsson **20080430171926] [Added _∈_. Nils Anders Danielsson **20080429110913] [Added map-∃ and map-∃₂. Nils Anders Danielsson **20080429020031] [Documented the associativity of _$_ and _<$>_. Nils Anders Danielsson **20080424131438] [Added a variant of gcd. Renamed gcd to gcd⁺. Nils Anders Danielsson **20080416162955] [Worked around Agda panic. Nils Anders Danielsson **20080416162812] [Added some missing files. Nils Anders Danielsson **20080416010754] [Changed to a more standard (?) definition of divisibility. Nils Anders Danielsson **20080416010745] [Added a variant of _divMod_. Renamed Result to DivMod. Nils Anders Danielsson **20080416000450] [Definition of coprimality, along with some properties. Nils Anders Danielsson **20080415185253] [Added 1-divides_. Nils Anders Danielsson **20080415184504] [Improved the interface. Nils Anders Danielsson **20080414194428] [Code for calculating the greatest common divisor. Nils Anders Danielsson **20080414182344] [Improved the interface. Nils Anders Danielsson **20080414182338] [Simplified the code by changing the definition of divisibility. Nils Anders Danielsson **20080414172703 + Having functions in indices is sometimes a bad idea. ] [Definition of divisibility, along with some properties. Nils Anders Danielsson **20080414170719] [Added a bunch of properties. Nils Anders Danielsson **20080414164933] [Improved (?) the interface of toDigits. Nils Anders Danielsson **20080414164919] [Added Fin-bounded. Nils Anders Danielsson **20080414164445] [Improved divMod's interface. Nils Anders Danielsson **20080412165041] [Changed the definition of _≗_. Nils Anders Danielsson **20080409213244 + Previously: f ≗ g = forall {x y} -> x ≡ y -> f x ≡ g y. Now: f ≗ g = forall x -> f x ≡ g x. ] [Tried changing to a different function type equality (in this module). Nils Anders Danielsson **20080409213220 + The "proper" solution is perhaps to use f ≗ g = forall {x y} -> x ≈₁ y -> f x ≈₂ g y, where _≗_ is parameterised on two equivalence relations _≈₁_ and _≈₂_; compare Data.List.Equality. However, this leads to rather heavy-weight code. I suspect that out of convenience the propositional equality _≡_ will be used for the lemmas in this module. In this case the current solution (the one above, but with _≡_ instead of _≈₁_/_≈₂_) seems unnecessarily complex. I prefer using f ≗ g = forall x -> f x ≡ g x, f ≗₂ g = forall x y -> f x y ≡ g x y, etc., just like Shin-Cheng did. Things would probably be a lot nicer if Agda had quotient types and extensional equality for functions. + Also generalised and renamed some functions. ] [Adding some more properties to Data.List.Properties scm@iis.sinica.edu.tw**20080407024038 Additions: foldr-universal, foldr-fusion, idIsFold, ++IsFold, mapIsFold, concat-map, map-compose, foldr-eq, map-eq. ] [Improved documentation. Broke out lemmas. Nils Anders Danielsson **20080409212249] [Added _∘′_. Nils Anders Danielsson **20080409202210] [Added Shin-Cheng Mu to the list of copyright holders. Nils Anders Danielsson **20080409193727] [Simplified the type of drop. Nils Anders Danielsson **20080408141722] [Added gfoldl and foldl. Nils Anders Danielsson **20080407202320] [Added foldl and foldl₁. Nils Anders Danielsson **20080407200831] [Removed 2*_, which is now unnecessary. Nils Anders Danielsson **20080407185543] [Proved that _*_ is monotone. Nils Anders Danielsson **20080407185458] [Changed the definition of _*_. Nils Anders Danielsson **20080407184806 + The new definition matches the one used by the Coq standard libraries, and Ulf's simple-lib. + Some things became more complicated, but overall the new definition seems to be a win. For instance, concat and group in Data.Vec are now defined without any auxiliary lemmas. Furthermore 2*_ can be defined in terms of _*_. ] [Fixed incorrect terminology. Nils Anders Danielsson **20080407161549] [Added foldr₁₀. Nils Anders Danielsson **20080401013236] [Added foldr₁. Nils Anders Danielsson **20080331233622] [Added 2*_. Nils Anders Danielsson **20080331134541] [Fixed comment. Nils Anders Danielsson **20080327115524] [Made curry and uncurry simply typed (except for the type arguments). Nils Anders Danielsson **20080326224912 + Renamed the dependently typed variants to Σ-curry and Σ-uncurry. ] [Improved documentation. Renamed some things. Nils Anders Danielsson **20080326162808] [Defined recursion structures etc. for subsets. Nils Anders Danielsson **20080326162602] [Added _⟶_. Nils Anders Danielsson **20080326162526] [Added _*2+1. Nils Anders Danielsson **20080326001843] [Added ≤-step. Nils Anders Danielsson **20080325220730] [Replaced n≤n+m with m≤m+n. Added m≤′m+n. Nils Anders Danielsson **20080325220335] [Simplified complete induction by using well-founded induction and a new ≤. Nils Anders Danielsson **20080325220238 + Now Logic.Induction.Nat.Examples.half₂ evaluates nicely. ] [Declared the fixity of if_then_else_. Nils Anders Danielsson **20080325220013] [Well-founded induction. Nils Anders Danielsson **20080325133411] [Proved that binary number equality is decidable. Nils Anders Danielsson **20080325041611] [Equality of lists. Nils Anders Danielsson **20080325040342] [A binary representation of natural numbers. Nils Anders Danielsson **20080325030949] [Defined ⌈_/2⌉ in terms of ⌊_/2⌋. Proved ⌊n/2⌋-mono and ⌈n/2⌉-mono. Nils Anders Danielsson **20080325030658] [Added Decimal, Bit, 0b and 1b. Nils Anders Danielsson **20080325025318] [Added fromDigits, renamed digits to toDigits and proved them correct. Nils Anders Danielsson **20080325010511] [Added addFin. Nils Anders Danielsson **20080325010127] [Added inject'. Nils Anders Danielsson **20080325010048] [Added init and last. Nils Anders Danielsson **20080325002125] [Made the witness argument to exists non-hidden. Nils Anders Danielsson **20080324233013] [Broke out Data.Digit from Data.Nat.Show. Nils Anders Danielsson **20080324192704] [Added ⌈n/2⌉≤n and ⌊n/2⌋≤n. Nils Anders Danielsson **20080324185911] [Enlarged the domain of _-_. Nils Anders Danielsson **20080324184416] [Added ⌈_/2⌉ and ⌊_/2⌋. Nils Anders Danielsson **20080324172443] [Added _div_ and _mod_. Nils Anders Danielsson **20080324164433] [Renamed Is to T. Nils Anders Danielsson **20080324153445] [Added boolToMaybe and maybeToBool. Nils Anders Danielsson **20080324015327] [Added toVec. Nils Anders Danielsson **20080324010608] [Added Data.Nat.Show. Nils Anders Danielsson **20080324010008] [Added witnessToTruth. Nils Anders Danielsson **20080324003818] [Added n≤n+m. Nils Anders Danielsson **20080324003802] [Added _≥_ and _>_. Nils Anders Danielsson **20080323231807] [Moved divMod to Data.Nat.DivMod. Proved it correct. Nils Anders Danielsson **20080323230907] [Added inject-lemma. Nils Anders Danielsson **20080323230853] [Made divMod structurally recursive. Nils Anders Danielsson **20080323183450] [Added _divMod_. Nils Anders Danielsson **20080323183444 + Note that the implementation is not structurally recursive. It is terminating, though. ] [Added some clarifying comments. Nils Anders Danielsson **20080323183233] [Improved <-rec's interface. Nils Anders Danielsson **20080323175004] [Added True and False. Nils Anders Danielsson **20080323131340] [Added Is. Nils Anders Danielsson **20080323130759] [Added compare and the Ordering view. Nils Anders Danielsson **20080323130506] [Added fixity declaration. Nils Anders Danielsson **20080323012347] [Added inject. Nils Anders Danielsson **20080322211401] [Vectors parameterised on things in Set1. Nils Anders Danielsson **20080322210949] [Renamed []₁ to [] and _∷₁_ to _∷_. Nils Anders Danielsson **20080322210924] [Added decToBool. Nils Anders Danielsson **20080322143327] [Generalised trivialAll, and renamed it to decorate. Nils Anders Danielsson **20080314044117] [Broke out Data.Star.Pointer from Data.Star.Decoration. Nils Anders Danielsson **20080314043620] [Added gmapAll and mapAll. Nils Anders Danielsson **20080314042740] [Added _◅◅◅_ and _▻▻▻_. Nils Anders Danielsson **20080314033649] [Added _▻_ and _▻▻_, renamed _◅▻_ to _◅◅_. Nils Anders Danielsson **20080314033129] [Renamed some lookup variants. Nils Anders Danielsson **20080314020022] [Added fromList and toList. Nils Anders Danielsson **20080313015403] [Added decoration and used it to simplify BoundedVec.toList. Nils Anders Danielsson **20080313015349] [Made NonEmpty a record type. Nils Anders Danielsson **20080313015015] [Added last. Nils Anders Danielsson **20080313012735] [Defined fromList and toList. Nils Anders Danielsson **20080313003124] [Defined init. Nils Anders Danielsson **20080313003103] [Defined bounded vectors using star-lists. Nils Anders Danielsson **20080313001353] [Generalised Any in order to be able to define bounded vectors. Nils Anders Danielsson **20080313001201] [Added map-NonEmpty. Nils Anders Danielsson **20080313000254] [Put the modules in alphabetical order. Nils Anders Danielsson **20080312211354] [Renamed dec to ↦. Nils Anders Danielsson **20080312210734] [Implemented heterogeneous collections in terms of star-lists. Nils Anders Danielsson **20080312210407 + Following McBride et al. ] [Generalised Data.Star.Lookup, following McBride et al. Nils Anders Danielsson **20080312210344 + This made vectors slightly less awkward to use. ] [Added Relation.Unary, containing Pred. Nils Anders Danielsson **20080312193715] [Added Const, Always, Never and NonEmpty. Nils Anders Danielsson **20080312193331] [Added McBride, Norell and Jansson's reflexive transitive closures. Nils Anders Danielsson **20080312192158 + (My adaptation.) ] [Minor simplification. Nils Anders Danielsson **20080312170935] [Added _⇒_, _=[_]⇒_, Sym and Trans. Renamed Refl to Reflexive. Nils Anders Danielsson **20080312165948] [Renamed mzero to ∅, ++ to ∣ and <*> to ⊛. Nils Anders Danielsson **20080312143831] [Made _IsRelatedTo_ public. Nils Anders Danielsson **20080312011700 + In order to make it easier to define customised variants of the library. ] [Added _≅₁_ and _≇₁_. Nils Anders Danielsson **20080311230821] [Defined reverse. Nils Anders Danielsson **20080307031425] [Minor simplification. Nils Anders Danielsson **20080307031205] [Added map₁₁ and foldr₁₁. Nils Anders Danielsson **20080306121850] [Updated copyright year notice. Nils Anders Danielsson **20080305193836] [Updated the library repository URL. Nils Anders Danielsson **20080305193816] [Removed listing of Algebra.RingSolver.Examples. Nils Anders Danielsson **20080305182851 + After I removed most uses of abstract this module takes far too long to type check. ] [Removed uses of abstract which were only inserted for efficiency reasons. Nils Anders Danielsson **20080305181948 + Reason: It is nice to be able to normalise proofs. + This change does imply longer type checking times, though. ] [Fixed name clashes. Nils Anders Danielsson **20080305165819] [Lists parameterised on things in Set1. Nils Anders Danielsson **20080305034024] [Added a variant of ∃. Nils Anders Danielsson **20080302214751 + Universe polymorphism would be very nice... ] [Added concat. Nils Anders Danielsson **20080229024849] [Added map. Nils Anders Danielsson **20080229023844] [Added singleton. Nils Anders Danielsson **20080226124010] [Added difference lists. Nils Anders Danielsson **20080226123810] [Reverted to the simply typed _∘_. Nils Anders Danielsson **20080225225300 + The dependently typed variants that I have tried are not drop-in replacements; there are situations in which the simply typed variant works and the others don't (without giving hidden arguments explicitly). If the library should single out a single variant to name, then I think it should be the simply typed one. ] [Generalised and simplified the code. Nils Anders Danielsson **20080223222850 + More results in fewer lines of code. ] [Changed the definition of a pointwise product of relations. Nils Anders Danielsson *-20080223214855 + A data type is used instead of a function. This means that more hidden arguments can be inferred automatically. + However, it also means that reusing code is harder, since a new type is introduced. I will revert to the previous definition. ] [Changed the definition of a pointwise product of relations. Nils Anders Danielsson **20080223214855 + A data type is used instead of a function. This means that more hidden arguments can be inferred automatically. + However, it also means that reusing code is harder, since a new type is introduced. I will revert to the previous definition. ] [Renamed <...>.PointWise to <...>.Pointwise. Nils Anders Danielsson **20080223212830] [Added missing "public" qualifier. Nils Anders Danielsson **20080223205713] [Added _-_. Nils Anders Danielsson **20080223205611] [Simplified and optimised downFrom. Nils Anders Danielsson **20080219151534] [Generalised the type of composition. Nils Anders Danielsson **20080219134650] [Added unfold and downFrom. Nils Anders Danielsson **20080219133657] [Fixed minor bug. Nils Anders Danielsson **20080212005132 + Previously Agda seems to have accepted this incorrect lemma. ] [Added a more flexible and heavyweight interface for equational reasoning. Nils Anders Danielsson **20080108191019] [Changed to the other (symmetric) formulation of associativity. Nils Anders Danielsson **20071211184819 + With the new formulation I do not need to use symmetry (or cast the "wrong" side of the law) when defining annotated monads, so I think it is a little more systematic. Note that the other formulation of associativity would be equally good, if the definition of identity was changed instead. ] [Noted that Data.Map/Data.Sets are not finished yet. Nils Anders Danielsson **20071211184420] [Added raw monoids. Nils Anders Danielsson **20071211164446] [Improved a comment. Nils Anders Danielsson **20071211163642] [Added semirings without an annihilating zero. Nils Anders Danielsson **20071211133618] [Fixed typo. Nils Anders Danielsson **20071211130214] [Corrected comment. Nils Anders Danielsson **20071211123410] [Simplified the definition of _*-NF_. Nils Anders Danielsson **20071211112939] [Proved that (ℕ, ⊔, ⊓, 0) is a commutative semiring without one. Nils Anders Danielsson **20071211104256] [Added commutative semirings without an identity element. Nils Anders Danielsson **20071211103924] [Added semirings without a unit element. Nils Anders Danielsson **20071211102136] [Added near-semirings. Nils Anders Danielsson **20071211100338] [Proved that (ℕ, ⊔, ⊓, 0) is a commutative monoid and a near-semiring. Nils Anders Danielsson **20071211095601] [Changed to another (equivalent) definition of distributive lattices. Nils Anders Danielsson **20071211095231 + The new one uses the same distributive law as the near-semirings. ] [Updated the Algebra hierarchy. Nils Anders Danielsson **20071207231200 + Now the Algebra record hierarchy is based on the same principles as those of Relation.Binary and Category. ] [Simplified the definition of reflexivity used by IsEquivalence. Nils Anders Danielsson **20071207231113] [Removed Data.Int and Algebra.RingSolver.Int. Nils Anders Danielsson **20071207225821 + They were broken due to an Agda bug, and I don't want to spend time maintaining code which does not type check. ] [Updated code to reflect changes in Relation.Binary. Nils Anders Danielsson **20071207223215] [Updated code to reflect changes in Relation.Binary.EqReasoning. Nils Anders Danielsson **20071207220851] [Added Fun₁ and Fun₂. Nils Anders Danielsson **20071207194053] [Instantiated PreorderReasoning for partial orders. Nils Anders Danielsson **20071207162129] [Added more conversions. Nils Anders Danielsson **20071207162034] [Created a separate module for _equational_ reasoning. Nils Anders Danielsson **20071207160950 + Moved the old EqReasoning to PreorderReasoning. ] [Removed empty directory. Nils Anders Danielsson **20071207155210] [Added some fixity declarations. Nils Anders Danielsson **20071207153128] [Improved layout. Nils Anders Danielsson **20071203081253] [Improved documentation of Core modules. Nils Anders Danielsson **20071203081238] [Got rid of the *Ops modules by using the new extended record declarations. Nils Anders Danielsson **20071203074250] [Simplified code using the new module instantiation syntax. Nils Anders Danielsson **20071203072429 + Also started making use of fixity declarations in record declarations. ] [Simplified the header file. Nils Anders Danielsson **20071130083514 + Moved some of the content to the Agda Wiki. ] [Added a simple README, pointing to the wiki. Nils Anders Danielsson **20071130034133] [Added script for creating the library documentation. Nils Anders Danielsson **20071130034025] [Added missing header. Nils Anders Danielsson **20071130034013] [Explained some impossible cases to make the completeness checker happy. Nils Anders Danielsson **20071129020415] [Updated code to reflect changes in Agda syntax. Nils Anders Danielsson **20071129020326 + The "field" keyword had to be inserted in record declarations. ] [Renamed *Nonstrict* to *NonStrict*. Nils Anders Danielsson **20071129015954] [Removed the synonyms Monotone and Monotone₂. Nils Anders Danielsson **20071128161443] [Merged EqReasoning and EqReasoning.Abstract. Nils Anders Danielsson **20071128160954 + Ulf informed me that one can reap the benefits of both libraries by using a data type instead of "abstract". ] [Improved comment. Nils Anders Danielsson **20071128155503] [Improved the structure of the Relation.Binary hierarchy. Nils Anders Danielsson **20071128155446 + Also made it easier to use, by creating modules which recursively reexport fields from subrecords. + Some missing pieces were also filled in. ] [Improved documentation. Nils Anders Danielsson **20071128155431] [Renamed _Preserves_,_ to _Preserves_→_. Nils Anders Danielsson **20071128020920 + And similarly for _Preserves₂_,_,_. ] [Sketched nice syntax for list constants. Nils Anders Danielsson *-20071127004524] [Sketched nice syntax for list constants. Nils Anders Danielsson **20071127004524] [Simplified the code a little. Nils Anders Danielsson **20071126152235] [The inefficient bounded vectors are back! (In a separate module.) Nils Anders Danielsson **20071126135638] [Added null. Nils Anders Danielsson **20071126110449] [Added filter. Nils Anders Danielsson **20071126110418] [Added foldl. Nils Anders Danielsson **20071126110413] [Added reverse. Nils Anders Danielsson **20071126103802] [The library is now licensed under the Expat licence. Nils Anders Danielsson **20071126063501] [Removed liftM₂. Nils Anders Danielsson **20071126001155] [Improved the performance of the bounded vectors (again). Nils Anders Danielsson **20071125143809 + Assuming that casts are erased. + Made them abstract and changed their representation. ] [Commented some code. Nils Anders Danielsson **20071125142810] [Connected the monads to the applicative functors. Nils Anders Danielsson **20071125142752 + Also made things more uniform. ] [Added functors and (indexed) applicative functors. Nils Anders Danielsson **20071125142400] [Moved the Monad hierarchy to Category.Monad. Nils Anders Danielsson **20071125135048] [state monads ulfn@cs.chalmers.se**20071121161839] [monads as special cases of indexed monads ulfn@cs.chalmers.se**20071120204215] [state and identity monads ulfn@cs.chalmers.se**20071120204141] [Improved layout. Nils Anders Danielsson **20071119164448] [Brought some code up to date. Nils Anders Danielsson **20071119162625] [Heterogeneous collections. Nils Anders Danielsson **20071119162433] [Renamed <*> to <$> and ap to <*> (to be consistent with Haskell libraries). Nils Anders Danielsson **20071119002616] [Improved the performance of the bounded vectors. Nils Anders Danielsson *-20071118015456 + Assuming that casts are erased. + Made them abstract and changed their representation. ] [Improved the performance of the bounded vectors. Nils Anders Danielsson **20071118015456 + Assuming that casts are erased. + Made them abstract and changed their representation. ] [Added toList and fromList. Nils Anders Danielsson **20071118013639] [Renamed zero to mzero. Nils Anders Danielsson **20071118012034] [Added bounded vectors. Nils Anders Danielsson **20071118011930] [Defined _ap_. Nils Anders Danielsson **20071117084334] [Renamed _<*_*>_ to liftM₂. Nils Anders Danielsson **20071117084319 + The name _<*_*>_ is not naturally related to _<*>_. ] [Added decidable setoids for characters and strings. Nils Anders Danielsson **20071116152417] [Added Data.Char and equality of strings. Nils Anders Danielsson **20071116150957] [Updated code since the name of a primitive changed. Nils Anders Danielsson **20071116144535] [Renamed liftM and liftM₂. Nils Anders Danielsson **20071115231231] [Defined what a (raw) monad is and defined the list and maybe monads. Nils Anders Danielsson **20071115225219] [Added concat. Nils Anders Danielsson **20071115194849] [Added an implementation of products using records. Nils Anders Danielsson **20071115193057] [Added some missing modules. Nils Anders Danielsson **20071023150256] [Created two versions of EqReasoning: with concrete or abstract equality. Nils Anders Danielsson **20071023145723] [Added ≡-subst-removable. Nils Anders Danielsson **20071016221300] [Added conversions between ≡ and ≅. Nils Anders Danielsson **20071016204429] [Proved m⊓n+n∸m≡n and i∸k∸j+j∸k≡i+j∸k. Nils Anders Danielsson **20071015111807] [Added m+n∸n≡m. Nils Anders Danielsson **20071002192434] [Added zip and zipWith. Nils Anders Danielsson **20071002160025] [Added head and tail. Nils Anders Danielsson **20071002155315] [Added concat. Nils Anders Danielsson **20071002104939] [Added group. Nils Anders Danielsson **20071002101149] [Broke out some core Vec definitions into Data.Vec.Core. Nils Anders Danielsson **20071002100210 + To enable using RingSolver in Data.Vec. ] [Stopped reexporting things from RingSolver. Nils Anders Danielsson **20071002095144] [Added splitAt. Nils Anders Danielsson **20071002092414] [Added drop. Nils Anders Danielsson **20071001155452] [Added length. Nils Anders Danielsson **20070928154442] [Defined the fixity of ≗. Nils Anders Danielsson **20070915174347] [Proved some properties for list-related functions. Nils Anders Danielsson **20070915150442] [Added sum. Nils Anders Danielsson **20070915150433] [Added id₁ and ∘₁. Nils Anders Danielsson **20070915150348] [Improved comment. Nils Anders Danielsson **20070828221620] [Started using the ... syntax for with clauses. Nils Anders Danielsson **20070814002933] [Commented out a module which is broken due to an Agda bug. Nils Anders Danielsson **20070814002845] [Made the equality reasoning library usable in more situations. Nils Anders Danielsson **20070814002559 + Now the library should handle equalities that evaluate better. (I have not tested this, though.) + Ulf informed me of the possibility of this improvement. ] [Addressed problem: Some things are no longer inferred automatically. Nils Anders Danielsson **20070814000827 + Due to magic with? ] [Defined vector equality. Proved some properties. Nils Anders Danielsson **20070713225043] [Made some lemmas concrete. Nils Anders Danielsson **20070711172953] [Proved n ∸ m ≤ n. Nils Anders Danielsson **20070710113254] [Added ≅-subst-removable. Nils Anders Danielsson **20070707212044] [Generalised some types. Nils Anders Danielsson **20070707211954] [Added convenient syntax for equality reasoning. Nils Anders Danielsson **20070707210532] [Added ≈-byDef. Nils Anders Danielsson **20070707180651] [Added _≈⟨_⟩_ and renamed _≃⟨_⟩_ to _∼⟨_⟩_. Nils Anders Danielsson **20070707174333] [Added +-mono. Nils Anders Danielsson **20070706151956] [Added Monotone₂. Nils Anders Danielsson **20070706151949] [Added some examples. Nils Anders Danielsson **20070705133831] [Broke out induction examples and added complete induction based on <. Nils Anders Danielsson **20070705125258] [Added <. Nils Anders Danielsson **20070705125114] [Added n≤1+n and n≤m+n. Nils Anders Danielsson **20070704235828] [Added ≤-Reasoning, a module for inequational reasoning. Nils Anders Danielsson **20070704234743] [Generalised definition of PreSetoid. Nils Anders Danielsson **20070704234642 + Now all partial orders are pre-setoids. + Moved some conversion functions to a separate module. ] [Defined + and * directly instead of using a fold. Nils Anders Danielsson **20070703113415 + Why? It is easier to read "m + n" than "fold n suc m" in a goal type. ] [Added sum. Nils Anders Danielsson **20070701232115] [Added take. Nils Anders Danielsson **20070701222730] [Improved documentation and structure of induction modules. Nils Anders Danielsson **20070701221022] [Added abstraction of various forms of recursion/induction. Nils Anders Danielsson **20070701215802 + Also proved general result about lexicographic induction. ] [Implemented convenient equality reasoning for ≡. Nils Anders Danielsson **20070630223716] [Added pointwise equality. Nils Anders Danielsson **20070630201813] [Proved m ⊓ n ≤ m. Nils Anders Danielsson **20070627183356] [Proved m + (n ∸ m) ≡ n. Nils Anders Danielsson **20070627181053] [Fixed minor bug. Nils Anders Danielsson **20070627180223] [Created a module for properties related to Fin. Nils Anders Danielsson **20070627180108] [Renamed ℕ-≤ to ≤. Nils Anders Danielsson **20070627175815] [Renamed Data.Fin.Props to Data.Fin.Subset.Props. Nils Anders Danielsson **20070627175528] [Made a bunch of proofs nonabstract. Nils Anders Danielsson **20070627142015 + It can be convenient if ≡-subst evaluates. Furthermore its RHS is shorter than its LHS. ] [After commenting out some code Algebra.RingSolver.Examples now works. Nils Anders Danielsson **20070627094829] [The semantics of open/import has changed. Nils Anders Danielsson **20070627094805 + So some code had to be updated. ] [The default associativity of operators has changed. Nils Anders Danielsson **20070627094712 + So some code had to be updated. ] [Proved some properties about the heterogeneous equality. Nils Anders Danielsson **20070626170920] [Sketched an interface for metaprogramming. Nils Anders Danielsson *-20070626153908 + It turned out to be unsound, though. ] [Sketched an interface for metaprogramming. Nils Anders Danielsson **20070626153908 + It turned out to be unsound, though. ] [Added ≡-subst₁. Nils Anders Danielsson **20070626153827] [Fixed a bunch of unsolved metas. Nils Anders Danielsson **20070626143810 + These were solved fine when Σ was a record, but started misbehaving when I changed Σ into a data type. ] [Commented out code due to bug in Agda's treatment of builtin integers. Nils Anders Danielsson **20070626125628] [Made code structurally recursive. Nils Anders Danielsson **20070626125534] [Rearranged things a little. Nils Anders Danielsson **20070626120538] [Added heterogeneous equality. Nils Anders Danielsson **20070626120526] [Added conversions to and from natural numbers. Nils Anders Danielsson **20070621172827] [Added function subtracting element of Fin n from n. Nils Anders Danielsson **20070621172549] [Renamed Π to Σ. Nils Anders Danielsson **20070621165058 + Since a product is a dependent sum... + Σ and ∃ could be merged, but I prefer to keep them separate (for now, anyway), since they are used in different ways. ] [Converted ⊤ into a record. Nils Anders Danielsson **20070620170927] [Added code for finite subsets. Nils Anders Danielsson **20070620151504] [Broke up Relation.Nullary into several modules. Nils Anders Danielsson **20070619221807] [Added finite maps and sets (currently postulated). Nils Anders Danielsson **20070619220332] [Added the inspect idiom. Nils Anders Danielsson **20070619214050] [Converted Π into a data type. Nils Anders Danielsson **20070619194507] [Made the combinators deciding × and ⊎ infix. Nils Anders Danielsson **20070619192428] [Exported the product projections from Data.Product. Nils Anders Danielsson **20070619191910] [Added some negated variants of ∃. Nils Anders Danielsson **20070619175855] [Exported some modules to make the module easier to use. Nils Anders Danielsson **20070619174922] [Turned ∃ into a data type. Nils Anders Danielsson **20070619174821] [Added some lemmas and definitions related to ¬. Nils Anders Danielsson **20070619162801] [Moved Dec to Relation.Nullary, proved some lemmas. Nils Anders Danielsson **20070619162745] [Improved comment. Nils Anders Danielsson **20070619150223] [Reorganised the library. Nils Anders Danielsson **20070618185135] [Simplified some code by making use of newly added primitives. Nils Anders Danielsson **20070618160919] [Added characters. Nils Anders Danielsson **20070618160451] [Generalised the ring solver. Nils Anders Danielsson **20070618132432 + The coefficients can now belong to a different ring-like structure. ] [Defined what a ring homomorphism is. Nils Anders Danielsson **20070618132205 + Also added "bare" rings. ] [Added postulated machine integers. Nils Anders Danielsson **20070618131458] [Started on an inductive representation of integers. Nils Anders Danielsson **20070618131444] [Added another example. Nils Anders Danielsson **20070618105111] [Added ++. Nils Anders Danielsson **20070618104956] [Generalised the semiring solver to a ring or semiring solver. Nils Anders Danielsson **20070617111117 + Introduced "almost commutative rings" to avoid code duplication. ] [Implemented solver for commutative semiring equalities. Nils Anders Danielsson **20070616222055] [Defined distributive lattices, proved some properties. Nils Anders Danielsson **20070616222020] [Changed fixity of xor. Nils Anders Danielsson **20070616221959] [Defined commutative rings and some conversions. Nils Anders Danielsson **20070616165700] [Cleaned up. Nils Anders Danielsson **20070616163713] [Improved file structure. Added some results. Nils Anders Danielsson **20070616162221] [Defined commutative semirings. Nils Anders Danielsson **20070616161639] [Renamed _⊕_ to _xor_. Nils Anders Danielsson **20070616014156] [Proved that the operations preserve equality. Nils Anders Danielsson **20070615223404] [Simplified boolean algebra construction. Nils Anders Danielsson **20070615172922] [Generalised the ring construction. Nils Anders Danielsson **20070615172845 + It is now parameterised over an xor operation. ] [Described how rings can be constructed from boolean algebras. Nils Anders Danielsson **20070615171059] [Proved that (∨, ∧, not, true, false) forms a boolean algebra. Nils Anders Danielsson **20070615170953] [Defined boolean algebras and proved some properties. Nils Anders Danielsson **20070615165750] [Added exclusive or. Nils Anders Danielsson **20070615101620] [Proved that ∧ and ∨ form a lattice. Nils Anders Danielsson **20070615101539] [Added minimum and maximum. Nils Anders Danielsson **20070615101443] [Defined lattices and some other properties. Nils Anders Danielsson **20070615101402] [Defined multiplication by natural number and exponentiation. Nils Anders Danielsson **20070615101322] [Added raise. Nils Anders Danielsson **20070614224243] [Added lookup. Nils Anders Danielsson **20070614221312] [Added more Bool operations and properties. Nils Anders Danielsson **20070614214515] [Minor cleanup. Nils Anders Danielsson **20070614211100] [Proved that (ℕ, +, *, 0, 1) forms a semiring. Nils Anders Danielsson **20070614203313] [Improved comments. Nils Anders Danielsson **20070614182715] [Proved some derived ring properties. Nils Anders Danielsson **20070614181729] [Algebraic properties packaged up with operations. Nils Anders Danielsson **20070614181435] [Some algebraic structures. Nils Anders Danielsson **20070614181316] [Added setoid⟶preSetoid. Nils Anders Danielsson **20070614181010] [Added Fin-setoid and other structures. Nils Anders Danielsson **20070614164447] [Invoked BUILTIN machinery for ∸. Nils Anders Danielsson **20070614164435] [Added byDef. Nils Anders Danielsson **20070614164327] [Rearranged things a bit. Nils Anders Danielsson **20070614142130] [Clarified proofs by using PreorderProof. Nils Anders Danielsson **20070614125429] [Added convenient syntax for preorder proofs. Nils Anders Danielsson **20070614125405 + À la Ulf Norell's EqProof module. ] [Added PreSetoid. Nils Anders Danielsson **20070614125304] [Moved ≈-resp-≤ from Poset to PartialOrder. Nils Anders Danielsson **20070614115707 + And added ≈-resp-< to StrictPartialOrder. ] [Proved a bunch of arithmetical equalities for natural numbers. Nils Anders Danielsson **20070614111640] [Added *. Nils Anders Danielsson **20070613191012] [Added Congruential₂. Nils Anders Danielsson **20070613191004] [Added Set1 version of ≡. Nils Anders Danielsson **20070613165421] [Minor fix. Nils Anders Danielsson **20070613160258] [Added ∸. Nils Anders Danielsson **20070613144959] [Added vectors. Nils Anders Danielsson **20070613144946] [Created a separate repository for the RegExp prelude. Nils Anders Danielsson **20070613143422 + Since I intend to use it in several projects. ] [Added boring file. Nils Anders Danielsson **20070613143342] >