Skip to content

spellchecked CHANGELOG #2078

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Sep 12, 2023
Merged

spellchecked CHANGELOG #2078

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a58cee7
spellchecked `CHANGELOG`
jamesmckinna Aug 31, 2023
8fc2ddd
removed spurious module entry
jamesmckinna Sep 1, 2023
3e3d693
Update CHANGELOG.md
jamesmckinna Sep 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 11 additions & 16 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -411,7 +411,7 @@ Non-backwards compatible changes
* At the moment, there are 4 different ways such instance arguments can be provided,
listed in order of convenience and clarity:
1. *Automatic basic instances* - the standard library provides instances based on the constructors of each
numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n`
numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constrains an instance of `NonZero (suc n)` for any `n`
and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently,
if the argument is of the required form, these instances will always be filled in by instance search
automatically, e.g.
Expand Down Expand Up @@ -589,7 +589,7 @@ Non-backwards compatible changes
```

* A new module `Reflection.AST` that re-exports the contents of the
submodules has been addeed.
submodules has been added.

### Implementation of division and modulus for `ℤ`

Expand Down Expand Up @@ -617,7 +617,7 @@ Non-backwards compatible changes
* `IsSemiringWithoutAnnihilatingZero`
* `IsRing`
* To aid with migration, structures matching the old style ones have been added
to `Algebra.Structures.Biased`, with conversionFunctions:
to `Algebra.Structures.Biased`, with conversion functions:
* `IsNearSemiring*` and `isNearSemiring*`
* `IsSemiringWithoutOne*` and `isSemiringWithoutOne*`
* `IsSemiringWithoutAnnihilatingZero*` and `isSemiringWithoutAnnihilatingZero*`
Expand All @@ -634,7 +634,7 @@ Non-backwards compatible changes
⊥ = Irrelevant Empty
```
in order to make ⊥ proof irrelevant. Any two proofs of `⊥` or of a negated
statements are now *judgementally* equal to each other.
statements are now *judgmentally* equal to each other.

* Consequently we have modified the following definitions:
+ In `Relation.Nullary.Decidable.Core`, the type of `dec-no` has changed
Expand Down Expand Up @@ -671,14 +671,14 @@ Non-backwards compatible changes
however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access
it now.

* In order to facilitate this reorganisation the following breaking moves have occured:
* In order to facilitate this reorganisation the following breaking moves have occurred:
- `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core`
- `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
- `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation`
to `Relation.Nullary.Decidable`.
- `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`.
- `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`.

### Refactoring of the unindexed Functor/Applicative/Monad hiearchy
### Refactoring of the unindexed Functor/Applicative/Monad hierarchy

* The unindexed versions are not defined in terms of the named versions anymore

Expand All @@ -698,7 +698,7 @@ Non-backwards compatible changes

* `MonadT T` now returns a `MonadTd` record that packs both a proof that the
`Monad M` transformed by `T` is a monad and that we can `lift` a computation
`M A` to a trasnformed computation `T M A`.
`M A` to a transformed computation `T M A`.

* The monad transformer are not mere aliases anymore, they are record-wrapped
which allows constraints such as `MonadIO (StateT S (ReaderT R IO))` to be
Expand Down Expand Up @@ -789,12 +789,12 @@ Non-backwards compatible changes
previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`.

* In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`,
`IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to
`IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redesigned to
build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and
`IsSemiringHomomorphism` respectively, adding a single property at each step.
This means that they no longer need to have two separate proofs of
`IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as
`IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic.
`IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homomorphic.

Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`.

Expand Down Expand Up @@ -939,7 +939,7 @@ Major improvements

* To fix this, these operators have been moved to `Data.Nat.Base`. The properties
for them still live in `Data.Nat.DivMod` (which also publicly re-exports them
to provide backwards compatability).
to provide backwards compatibility).

* Beneficiaries of this change include `Data.Rational.Unnormalised.Base` whose
dependencies are now significantly smaller.
Expand Down Expand Up @@ -1604,11 +1604,6 @@ New modules
Data.List.NonEmpty.Relation.Unary.All
```

* A small library for heterogenous equational reasoning on vectors:
```
Data.Vec.Properties.Heterogeneous
```

* Show module for unnormalised rationals:
```
Data.Rational.Unnormalised.Show
Expand Down