agda2hs-1.4: CHANGELOG.md

Release notes for agda2hs v1.4
==============================

Changes
-------

Changes to agda2hs:
- Increased Agda base version to 2.8.
- Increased bounds to support GHC 9.12.2.
- agda2hs will now skip compilation of files that are up-to-date.
- Added support for multi-parameter type classes.
- Added support for quantified constraints.
- Agda record types that compile to a Haskell data type are now
  required to have the `no-eta-equality` directive.
- agda2hs will now assume that any modules under the `Haskell.`
  namespace are part of the trusted FFI with Haskell.
  Concretely, no code will be generated for these modules and
  the `Haskell.` prefix will be dropped from the module name.

Additions to the agda2hs Prelude:
- The builtin sort `Set` has been renamed to `Type` in the agda2hs Prelude
- The `Rezz` type defined in `Haskell.Extra.Erase` has been renamed to `Singleton`.
- The bindings to the Haskell `base` library are now located under `lib/base`
  to allow for adding bindings to other Haskell libraries.
- Added new module `Haskell.Control.Exception` with the `assert` function
  which can be used to assert any decidable property, with the decidability
  proof being compiled to a boolean check in Haskell.
- Added new module `Haskell.Data.Maybe` with `fromMaybe` and other functions.
- Added new module `Haskell.Data.List` with functions `nub`, `deleteAll`, and `sort`
  together with some of their properties.
- Added new modules `Haskell.Data.Map` and `Haskell.Data.Set` from the
  `containers` package, together with a number of their properties.
  These libraries are part of the new `containers` package located in `lib/containers`.
- Added properties of boolean values and operations under `Haskell.Law.Bool`.
- Added laws for the `Num` type class and its instances under `Haskell.Law.Num`.


See https://github.com/agda/agda2hs/issues?q=milestone%3A1.4+is%3Apr for the full list of changes.

Fixed issues
------------

See https://github.com/agda/agda2hs/issues?q=milestone%3A1.4+is%3Aissue for the full list of fixed issues.