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

Define adjunction with nicer type (cf., #68) #74

Open
nateyazdani opened this issue Sep 15, 2019 · 1 comment
Open

Define adjunction with nicer type (cf., #68) #74

nateyazdani opened this issue Sep 15, 2019 · 1 comment
Labels
enhancement New feature or request help wanted Extra attention is needed

Comments

@nateyazdani
Copy link
Contributor

As mentioned in the PR for auto-instantiated adjunction proofs (#68), the constant for each adjunction proof should be assigned a nicer type for the user. Currently, the type inferred by Coq refers to the fg_id' lemma, rather than the nice wrapper ${ornament}_retraction for an ornament ${ornament}.

This task is not technically challenging but involves a lot of annoying plumbing in OCaml to assemble the desired type.
@nateyazdani nateyazdani added the enhancement New feature or request label Sep 15, 2019
@nateyazdani nateyazdani mentioned this issue Sep 15, 2019
Merged
@tlringer tlringer added the help wanted Extra attention is needed label Sep 17, 2020
@tlringer
Copy link
Collaborator

Nate has moved on to other things, so help improving this is always welcome.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request help wanted Extra attention is needed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nateyazdani @tlringer