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.

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

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

Merged
merged 2 commits into from
Jul 14, 2024

Conversation

joelberkeley
Copy link
Contributor

@joelberkeley joelberkeley commented Jul 13, 2024

I'm using this to provide more informative proofs on function arguments than IsJust.

libs/base/Data/Either.idr Show resolved Hide resolved
libs/base/Data/Either.idr Show resolved Hide resolved
@andrevidela
Copy link
Collaborator

Looks good

@andrevidela andrevidela merged commit 182bcff into idris-lang:main Jul 14, 2024
22 checks passed
@joelberkeley joelberkeley deleted the fromrightleft branch July 14, 2024 16:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants