Refactor graphs with updates from Beyond finite sets #879
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Comment on lines
538
to
546
| has-decidable-equality-walk-Undirected-Graph-𝔽 : | ||
| {x y : vertex-Undirected-Graph-𝔽 G} → | ||
| has-decidable-equality (walk-Undirected-Graph-𝔽 G x y) | ||
| has-decidable-equality-walk-Undirected-Graph-𝔽 {x} {.x} | ||
| refl-walk-Undirected-Graph w = | ||
| {!!} | ||
| has-decidable-equality-walk-Undirected-Graph-𝔽 {x} {._} | ||
| ( cons-walk-Undirected-Graph p e v) w = | ||
| {!!} |
There was a problem hiding this comment.
Oh yeah, I left some holes. Gotta fix that!
There was a problem hiding this comment.
I was going to merge this PR as I thought this was cleaned up. But I see this still isn't, so I'll leave it for you to finish first.
fredrik-bakke
approved these changes
Oct 22, 2023
Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
Your comments look good too |
Thanks! I wrote them just for you :) |
|
Hey, @EgbertRijke, as far as I can tell from the comments on this PR it is very close to ready for merging. Perhaps the outstanding formalizations can be left for a future PR so we can merge this one? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR refactors the graph theory library with updates from the Beyond Finite Sets PR.