From 0ed19f3630a80a85f17e220bc3150039fb909233 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Sat, 13 Jul 2024 22:57:31 +0100
Subject: [PATCH 1/2] add `fromRight` and `fromLeft` for extracting values out
 of `Either`

---
 libs/base/Data/Either.idr | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/libs/base/Data/Either.idr b/libs/base/Data/Either.idr
index c0b17dd6a..ae1f78260 100644
--- a/libs/base/Data/Either.idr
+++ b/libs/base/Data/Either.idr
@@ -41,6 +41,11 @@ export
 Uninhabited (IsRight (Left x)) where
   uninhabited ItIsRight impossible
 
+||| Returns the `r` value of an `Either l r` which is proved `Right`.
+fromRight : (e : Either l r) -> {auto 0 isRight : IsRight e} -> r
+fromRight (Right r) = r
+fromRight (Left _) impossible
+
 ||| Proof that an `Either` is actually a Left value
 public export
 data IsLeft : Either a b -> Type where
@@ -50,6 +55,11 @@ export
 Uninhabited (IsLeft (Right x)) where
   uninhabited ItIsLeft impossible
 
+||| Returns the `l` value of an `Either l r` which is proved `Left`.
+fromLeft : (e : Either l r) -> {auto 0 isLeft : IsLeft e} -> l
+fromLeft (Right _) impossible
+fromLeft (Left l) = l
+
 --------------------------------------------------------------------------------
 -- Grouping values
 

From 3a43c135c8025b87aa5bb0e85db09ab88c8fa745 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Sat, 13 Jul 2024 22:59:51 +0100
Subject: [PATCH 2/2] changelog

---
 CHANGELOG_NEXT.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index c79154542..c9ad69f79 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -198,6 +198,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Quantity of the argument for the type being searched in the `search` function
   from `Language.Reflection` was changed to be zero.
 
+* Added `fromRight` and `fromLeft` for extracting values out of `Either`, equivalent to `fromJust` for `Just`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.