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

Rename inc/ouc everywhere #3714

Closed
mortberg opened this issue Apr 24, 2019 · 3 comments · Fixed by #6032
Closed

Rename inc/ouc everywhere #3714

mortberg opened this issue Apr 24, 2019 · 3 comments · Fixed by #6032
Assignees
@plt-amy
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp documented-in-changelog Issues already documented in the CHANGELOG type: enhancement Issues and pull requests about possible improvements
Milestone
2.6.3

Comments

@mortberg
Copy link
Collaborator

The cubical primitive primSubOut is currently called ouc in many of the builtin files and the reference manual. This was chosen to match its inverse primitive inc. However, this has caused quite a bit of confusion and I've lost track by how many times someone asked me what ouc stands for (maybe "ouclusion"?). Because of this we renamed them to inS and outS in the agda/cubical library. I would suggest that we make the naming consistent and use inS/outS everywhere unless someone has a better suggestion.
@mortberg mortberg added the cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp label Apr 24, 2019
@mortberg mortberg self-assigned this Apr 24, 2019
@jespercockx jespercockx added the type: enhancement Issues and pull requests about possible improvements label Nov 18, 2019
@jespercockx jespercockx added this to the 2.6.1 milestone Nov 18, 2019
@jespercockx
Copy link
Member

@mortberg do you have time to work on this before the release later this month? If not, please update the milestone to 2.6.2.

@mortberg mortberg modified the milestones: 2.6.1, 2.6.2 Dec 3, 2019
@nad
Copy link
Contributor

nad commented Apr 8, 2021

@mortberg, do you still want to make this change?

@mortberg
Copy link
Collaborator Author

mortberg commented Apr 8, 2021

It would be good to do it, but I don't have the time to do it now. It should be very easy to fix though, just rename inc to inS and ouc to outS

@nad nad modified the milestones: 2.6.2, icebox Apr 8, 2021
@plt-amy plt-amy mentioned this issue Aug 9, 2022
Closed
@plt-amy plt-amy mentioned this issue Aug 16, 2022
Merged
@jespercockx jespercockx modified the milestones: icebox, 2.6.3 Aug 24, 2022
@jespercockx jespercockx assigned plt-amy and unassigned mortberg Aug 24, 2022
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
plt-amy added a commit that referenced this issue Oct 24, 2022
@plt-amy
re #6055: fixed changelogs for #3714; #5827, #6219
7a63062 
Also removes the mention of copatterns not being supported from the Agsy
docs
@andreasabel andreasabel added the documented-in-changelog Issues already documented in the CHANGELOG label Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@plt-amy plt-amy

Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp documented-in-changelog Issues already documented in the CHANGELOG type: enhancement Issues and pull requests about possible improvements
Projects
None yet
Milestone
2.6.3
5 participants
@nad @mortberg @andreasabel @jespercockx @plt-amy