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

[ new ] Data.OpenUnion #1050

Merged
merged 6 commits into from Feb 10, 2021
Merged

[ new ] Data.OpenUnion #1050

merged 6 commits into from Feb 10, 2021

Conversation

gallais
Copy link
Member

@gallais gallais commented Feb 9, 2021

Had to introduce this while looking at Freer and figured it may see good use in contrib too.
Note that this is the open union of families. But we could equally well define the open
union of types.

Similar to the ones used in the Freer paper, except everythins is
proven safe.
@gallais gallais merged commit 8ba3d85 into idris-lang:master Feb 10, 2021
@gallais gallais deleted the libs-galore branch February 10, 2021 15:25
andrevidela pushed a commit to andylokandy/Idris2 that referenced this pull request Feb 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants