Merge pull request #3348 from joelberkeley/fromrightleft

Add `fromRight` and `fromLeft` for extracting values out of `Either`

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`.

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