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

FunExt implies WeakFunExt #74

Merged
merged 8 commits into from
Oct 3, 2023
Merged

FunExt implies WeakFunExt #74

merged 8 commits into from
Oct 3, 2023

Conversation

MatthiasHu
Copy link
Contributor

@MatthiasHu MatthiasHu commented Sep 28, 2023 •
edited
Loading

Part of #73.

@MatthiasHu MatthiasHu mentioned this pull request Sep 28, 2023
Open
@MatthiasHu
Copy link
Contributor Author

This is only a draft pull request for now. I am grateful for any comments/corrections of course!

emilyriehl
emilyriehl reviewed Sep 29, 2023
View reviewed changes
Copy link
Collaborator

@emilyriehl emilyriehl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good. If you want to clean it up (deleting the todos and the hole) we could merge this part now and you could start a new PR for the rest. But in that case you should edit your comment above to say "part of #74" rather than "closes" because I think github might automatically close the issue otherwise.

src/hott/06-contractible.rzk.md Outdated Show resolved Hide resolved
src/hott/06-contractible.rzk.md Outdated Show resolved Hide resolved
@MatthiasHu MatthiasHu changed the title WeakFunExt vs FunExt FunExt implies WeakFunExt Sep 29, 2023
@MatthiasHu MatthiasHu marked this pull request as ready for review September 29, 2023 10:29
@MatthiasHu
Copy link
Contributor Author

This is ready now.

Is the name map-for-weakfunext ok?

@jonweinb
Copy link
Collaborator

jonweinb commented Oct 1, 2023

This is ready now.

Is the name map-for-weakfunext ok?

I'd go for map-for-weakfunext according to previous conventions. Otherwise, I can merge.

@MatthiasHu
Copy link
Contributor Author

Sorry -- are you saying the name should be changed, or are you saying it can stay as it is?

@jonweinb
Copy link
Collaborator

jonweinb commented Oct 1, 2023

Oops, sorry for the typo. I think map-weakfunext is more in line with preexisting conventions than map-for-weakfunext, so arguing for a change.

@MatthiasHu
Copy link
Contributor Author

Thanks, I changed it.

@emilyriehl emilyriehl merged commit 5e8843c into rzk-lang:main Oct 3, 2023
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@emilyriehl emilyriehl emilyriehl left review comments

@jonweinb jonweinb jonweinb approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@MatthiasHu @jonweinb @emilyriehl