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

Find a way to generalise TNat1 and TString1 #235

Open
andrevidela opened this issue Jun 21, 2020 · 0 comments
Open

Find a way to generalise TNat1 and TString1 #235

andrevidela opened this issue Jun 21, 2020 · 0 comments
Labels
feature:enhancement Enhancements that do not affect core functionality newcomer:help wanted This issue needs a new pair of eyes

Comments

@andrevidela
Copy link
Collaborator

In the API exposed for Idris, we expose the specialised types TNat and TString as well as counterparts that take a single type argument, but do not do anything with it (TNat1 and TString).
This is used when combining specialised types in products and sums which take type arguments.

However we cannot implement those for all possible arities. Therefore, we need to find a way to generalise this pattern and automatically weaken/strengthen the index of such references.
@andrevidela andrevidela added backend feature:enhancement Enhancements that do not affect core functionality newcomer:help wanted This issue needs a new pair of eyes labels Jun 23, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature:enhancement Enhancements that do not affect core functionality newcomer:help wanted This issue needs a new pair of eyes
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@andrevidela