idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #3348 from joelberkeley/fromrightleft

Browse Source 
Add `fromRight` and `fromLeft` for extracting values out of `Either`
This commit is contained in:
André Videla 2024-07-14 15:21:01 +01:00 committed by GitHub
commit 182bcff0ff
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG_NEXT.md
View File

@ -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 * Quantity of the argument for the type being searched in the `search` function
from `Language.Reflection` was changed to be zero. from `Language.Reflection` was changed to be zero.
* Added `fromRight` and `fromLeft` for extracting values out of `Either`, equivalent to `fromJust` for `Just`.
#### Contrib #### Contrib
* `Data.List.Lazy` was moved from `contrib` to `base`. * `Data.List.Lazy` was moved from `contrib` to `base`.

10
libs/base/Data/Either.idr
View File

@ -41,6 +41,11 @@ export
Uninhabited (IsRight (Left x)) where Uninhabited (IsRight (Left x)) where
uninhabited ItIsRight impossible 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 ||| Proof that an `Either` is actually a Left value
public export public export
data IsLeft : Either a b -> Type where data IsLeft : Either a b -> Type where
@ -50,6 +55,11 @@ export
Uninhabited (IsLeft (Right x)) where Uninhabited (IsLeft (Right x)) where
uninhabited ItIsLeft impossible 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 -- Grouping values