Skip to content
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

Jump to bottom

Add fromRight and fromLeft for extracting values out of Either #3348

Merged
merged 2 commits into from
Jul 14, 2024
Merged

Add fromRight and fromLeft for extracting values out of Either #3348

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0ed19f3
add `fromRight` and `fromLeft` for extracting values out of `Either`
joelberkeley Jul 13, 2024
3a43c13
changelog
joelberkeley Jul 13, 2024
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
2 changes: 2 additions & 0 deletions CHANGELOG_NEXT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
10 changes: 10 additions & 0 deletions libs/base/Data/Either.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
andrevidela marked this conversation as resolved.
Show resolved Hide resolved
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
Expand All @@ -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
andrevidela marked this conversation as resolved.
Show resolved Hide resolved
fromLeft (Right _) impossible
fromLeft (Left l) = l

--------------------------------------------------------------------------------
-- Grouping values

Expand Down
Loading