-
Notifications
You must be signed in to change notification settings - Fork 0
Issues: jvanbruegge/binder_datatypes
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Adapt recursor for multiple bounds for single free position
new feature
Allows to define types that are currently impossible to define
#58
opened Nov 7, 2024 by
jvanbruegge
Make binder_inductive automation work in more (all?) cases
usability
Changes that will make it nicer for the end user
#57
opened Nov 5, 2024 by
jvanbruegge
Allow multiple kinds of variables in binder_inductive
good first issue
Good for newcomers
new feature
Allows to define types that are currently impossible to define
#47
opened Jul 31, 2024 by
jvanbruegge
Make parser work with mutual recursion
usability
Changes that will make it nicer for the end user
#41
opened Jul 7, 2024 by
jvanbruegge
1 task
Make sugar allow mutual recursion
new feature
Allows to define types that are currently impossible to define
usability
Changes that will make it nicer for the end user
#37
opened Feb 26, 2024 by
jvanbruegge
1 task done
Make sugar allow passive positions
new feature
Allows to define types that are currently impossible to define
usability
Changes that will make it nicer for the end user
#36
opened Feb 26, 2024 by
jvanbruegge
1 task done
Automate singular/list substitution
good first issue
Good for newcomers
new feature
Allows to define types that are currently impossible to define
usability
Changes that will make it nicer for the end user
#19
opened Oct 17, 2023 by
jvanbruegge
Make tvsubst compose
new feature
Allows to define types that are currently impossible to define
usability
Changes that will make it nicer for the end user
#12
opened Aug 29, 2023 by
jvanbruegge
3 tasks done
Implement the corecursor
new feature
Allows to define types that are currently impossible to define
#11
opened Aug 29, 2023 by
jvanbruegge
Allow changing the names of the involved constants
good first issue
Good for newcomers
usability
Changes that will make it nicer for the end user
#9
opened Aug 29, 2023 by
jvanbruegge
Create a binder_(co)primrec to define primitive recursive functions on binder_datatypes
research needed
There is no existing design for the feature
usability
Changes that will make it nicer for the end user
#8
opened Aug 29, 2023 by
jvanbruegge
2 tasks
ProTip!
Find all open issues with in progress development work with linked:pr.