Skip to content
This repository has been archived by the owner on Jun 4, 2021. It is now read-only.

a few Either functions #68

Closed
anovstrup opened this issue Sep 4, 2020 · 1 comment
Closed

a few Either functions #68

anovstrup opened this issue Sep 4, 2020 · 1 comment

Comments

@anovstrup
Copy link
Contributor

This PR adds Either.fold, Either.left, Either.right, and Either.unwrap functions with associated documentation. These definitions also appear in #57 (not yet reviewed/merged), but they did not include documentation in that PR. Tests are omitted, since the definitions are very simple and obviously correct.

Code review

The changes summarized below are available for you to review, using the following command:

pull-request.load https://github.com/unisonweb/base:.trunk https://github.com/anovstrup/unisonweb-base:.prs._either1

Added definitions:

 Either.fold       : ∀ o 𝕖 i1 i. (i1 ->{𝕖} o) -> (i ->{𝕖} o) -> Either i1 i ->{𝕖} o (+3 metadata)
 Either.fold.doc   : Doc (+2 metadata)
 Either.left       : Either l r -> Optional l (+3 metadata)
 Either.left.doc   : Doc (+2 metadata)
 Either.right      : Either l r -> Optional r (+3 metadata)
 Either.right.doc  : Doc (+2 metadata)
 Either.unwrap     : Either a a -> a (+3 metadata)
 Either.unwrap.doc : Doc (+2 metadata)
@runarorama
Copy link
Contributor

Merged in base hash #o6r70946gi. Thanks! 🌈⭐

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

No branches or pull requests

2 participants