CHANGELOG

------------------------------------------------------------------------
-- Release notes for Agda standard library version TODO
------------------------------------------------------------------------

The library has been tested using Agda version TODO.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

Important changes since 0.11:

* Added support for GHC 8.0.1.

------------------------------------------------------------------------
-- Release notes for Agda standard library version 0.11
------------------------------------------------------------------------

The library has been tested using Agda version 2.4.2.4.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

Important changes since 0.10:

* Relation.Binary.PropositionalEquality.TrustMe.erase was added.

* Added Data.Nat.Base.{_≤″_,_≥″_,_<″_,_>″_,erase},
  Data.Nat.Properties.{≤⇒≤″,≤″⇒≤}, Data.Fin.fromℕ≤″, and
  Data.Fin.Properties.fromℕ≤≡fromℕ≤″.

* The functions in Data.Nat.DivMod have been optimised.

* Turned on η-equality for Record.Record, removed Record.Signature′
  and Record.Record′.

* Renamed Data/AVL.agda._⊕_sub1 to pred[_⊕_].

------------------------------------------------------------------------
-- Release notes for Agda standard library version 0.10
------------------------------------------------------------------------

The library has been tested using Agda version 2.4.2.3.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

Important changes since 0.9:

* Renamed Data.Unit.Core to Data.Unit.NonEta

* Removed Data.String.Core.
  The module Data.String.Base now contains these definitions.

* Removed Relation.Nullary.Core.
  The module Relation.Nullary now contains these definitions directly.

* Inspect on steroids has been simplified (see
  Relation.Binary.PropositionalEquality and
  Relation.Binary.HeterogeneousEquality).

  The old version has been deprecated (see the above modules) and it
  will be removed in the next release.

* Using Data.X.Base modules.

  The Data.X.Base modules are used for cheaply importing a data type
  and the most common definitions. The use of these modules reduce
  type-checking and compilation times.

  At the moment, the modules added are:

  Data.Bool.Base
  Data.Char.Base
  Data.Integer.Base
  Data.List.Base
  Data.Maybe.Base
  Data.Nat.Base
  Data.String.Base
  Data.Unit.Base

  These modules are also cheap to import and can be considered basic:

  Data.BoundedVec.Inefficient
  Data.Empty
  Data.Product
  Data.Sign
  Data.Sum
  Function
  Level
  Relation.Binary
  Relation.Binary.PropositionalEquality.TrustMe
  Relation.Nullary

* Added singleton sets to Relation.Unary.

  There used to be an isomorphic definition of singleton sets in
  Monad.Predicate, this has been removed and the module has been
  cleaned up accordingly.

  The singleton set is also used to define generic operations
  (Plotkin and Power's terminology) in Data.Container.Indexed.FreeMonad.

* Proved properties of Data.List.gfilter.  The following definitions
  have been added to Data.List.Properties:

    gfilter-just      : ... → gfilter just xs ≡ xs
    gfilter-nothing   : ... → gfilter (λ _ → nothing) xs ≡ []
    gfilter-concatMap : ... → gfilter f ≗ concatMap (fromMaybe ∘ f)

* New in Data.Nat.Properties:

    <⇒≤pred : ∀ {m n} → m < n → m ≤ pred n

* New in Data.Fin:

   strengthen : ∀ {n} (i : Fin n) → Fin′ (suc i)

* New in Data.Fin.Properties:

   from-to        : ∀ {n} (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
   toℕ-strengthen : ∀ {n} (i : Fin n) → toℕ (strengthen i) ≡ toℕ i

   fromℕ-def    : ∀ n → fromℕ n ≡ fromℕ≤ ℕ≤-refl
   reverse-suc  : ∀{n}{i : Fin n} → toℕ (reverse (suc i)) ≡ toℕ (reverse i)
   inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ≤ n) → inject≤ i n≤n ≡ i

* New in Data.List.NonEmpty:

    foldr₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
    foldl₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A

* Data.AVL.Height-invariants._∼_ was replaced by _∼_⊔_, following
  Conor McBride's principle of pushing information into indices rather
  than pulling information out.

  Some lemmas in Data.AVL.Height-invariants (1+, max∼max and
  max-lemma) were removed.

  The implementations of some functions in Data.AVL were simplified.
  This could mean that they, and other functions depending on them (in
  Data.AVL, Data.AVL.IndexedMap and Data.AVL.Sets), reduce in a
  different way than they used to.

* The fixity of all _∎ and finally operators, as well as
  Category.Monad.Partiality.All._⟨_⟩P, was changed from infix 2 to
  infix 3.

* The fixity of Category.Monad.Partiality._≟-Kind_, Data.AVL._∈?_,
  Data.AVL.IndexedMap._∈?_, Data.AVL.Sets._∈?_, Data.Bool._≟_,
  Data.Char._≟_, Data.Float._≟_, Data.Nat._≤?_,
  Data.Nat.Divisibility._∣?_, Data.Sign._≟_, Data.String._≟_,
  Data.Unit._≟_, Data.Unit._≤?_ and
  Data.Vec.Equality.DecidableEquality._≟_ was changed from the default
  to infix 4.

* The fixity of all _≟<something>_ operators in Reflection is now
  infix 4 (some of them already had this fixity).

* The fixity of Algebra.Operations._×′_ was changed from the default
  to infixr 7.

* The fixity of Data.Fin.#_ was changed from the default to infix 10.

* The fixity of Data.Nat.Divisibility.1∣_ and _∣0 was changed from the
  default to infix 10.

* The fixity of Data.Nat.DivMod._divMod_, _div_ and _mod_ was changed
  from the default to infixl 7.

* The fixity of Data.Product.Σ-syntax was changed from the default to
  infix 2.

* The fixity of Relation.Unary._~ was changed from the default to infix
  10.

* Turned on η-equality for Record.Record, removed Record.Signature′
  and Record.Record′.

------------------------------------------------------------------------
-- Release notes for Agda standard library version 0.9
------------------------------------------------------------------------

The library has been tested using Agda version 2.4.2.1.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

Important changes since 0.8.1:

* Data.List.NonEmpty

  Non-empty lists are no longer defined in terms of Data.Product._×_,
  instead, now they are defined as record with fields head and tail.

* Reflection API

  ** Quoting levels was fixed. This fix could break some code (see
     Agda issue 1207).

  ** The Reflection.type function returns a normalised Reflection.Type
     and quoteTerm returns an η-contracted Reflection.Term now. These
     changes could break some code (see Agda issue 1269).

  ** The primitive function for showing names, primShowQName, is now
     exposed as Reflection.showName.

* Removed compatibility modules for Props -> Properties rename

  Use Foo.Properties.Bar instead of Foo.Props.Bar.

------------------------------------------------------------------------
-- Version 0.8.1
------------------------------------------------------------------------

The library has been tested using Agda version 2.4.2.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

Important changes since 0.8:

* Reflection API

  Agda 2.4.2 added support for literals, function definitions, pattern
  matching lambdas and absurd clause/patterns (see Agda release
  notes). The new supported entities were added to the Reflection.agda
  module.

* Modules renamed

  Foo.Props.Bar -> Foo.Properties.Bar

  The current compatibility modules Foo.Props.Bar will be removed in
  the next release.

------------------------------------------------------------------------
Version 0.8
------------------------------------------------------------------------

Version 0.8 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.4.0.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

------------------------------------------------------------------------
Version 0.7
------------------------------------------------------------------------

Version 0.7 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.3.2.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

-------------------------------------------------------------------
Version 0.6
------------------------------------------------------------------------

Version 0.6 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.3.0.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as
follows:

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler
backends.

------------------------------------------------------------------------
Version 0.5
------------------------------------------------------------------------

Version 0.5 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.2.10.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

------------------------------------------------------------------------
Version 0.4
------------------------------------------------------------------------

Version 0.4 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.2.8.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

------------------------------------------------------------------------
Version 0.3
------------------------------------------------------------------------

Version 0.3 of the standard library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.2.6.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

------------------------------------------------------------------------
Version 0.2
------------------------------------------------------------------------

Version 0.2 of the "standard" library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.2.4.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

Note also that the library sources are now located in the
sub-directory lib-<version>/src of the installation tarball.

------------------------------------------------------------------------
Version 0.1
------------------------------------------------------------------------

Version 0.1 of the "standard" library has now been released, see
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.

The library has been tested using Agda version 2.2.2.

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.