From 2b088a4eb4401bb9272c85f0676c8193a3f19f43 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 17 Sep 2022 13:26:50 +0100 Subject: [PATCH] Update CHANGELOG.md This corrects an error in the `CHANGELOG` for PR#1735, which left a dangling reference to the old `Category.*` hierarchy. --- CHANGELOG.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b647d5114..fb08ee75d8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1224,13 +1224,6 @@ Other minor changes record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) ``` -* Added new functions in `Category.Monad.State`: - ``` - runState : State s a → s → a × s - evalState : State s a → s → a - execState : State s a → s → s - ``` - * Added new proofs in `Data.Bool.Properties`: ```agda <-wellFounded : WellFounded _<_ @@ -1676,6 +1669,13 @@ Other minor changes ++-assoc : (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) ``` +* Added new functions in `Effect.Monad.State`: + ``` + runState : State s a → s → a × s + evalState : State s a → s → a + execState : State s a → s → s + ``` + * Added new proofs in `Function.Construct.Symmetry`: ``` bijective : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹