-
Notifications
You must be signed in to change notification settings - Fork 47
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
Wedges part 1 #1384
Wedges part 1 #1384
Conversation
Shouldn't |
In this commit , the |
I ended up with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the last commit, I just fixed the changelog and I also took the liberty to rename wedge_lift_p0E
to wedge_liftE
because p0
is a local variable that I think should not be exposed. You may want to change that to a better name.
A rather important construction for homotopies, this makes progress towards getting #1350 broken into smaller chunks
Checklist
CHANGELOG_UNRELEASED.md
Reference: How to document
Reminder to reviewers