Union, Intersection, Set Difference and Further Operations on Indexed Sets #92
Conversation
This file contains hidden or 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
pmbittner
force-pushed
the
isetops-fixed
branch
from
9d7aa59 to
1b05961
Compare
ibbem
requested changes
Oct 7, 2025
Collaborator
ibbem
left a comment
ibbem
left a comment
There was a problem hiding this comment.
There is also a variable declaraction at the top of the IndexedSet file which also should be changed to private.
Moving proofs into a separate Properties submodule sound like a godd idea indeed.
pmbittner
force-pushed
the
isetops-fixed
branch
2 times, most recently
from
1270497 to
038b18b
Compare
pmbittner
force-pushed
the
isetops-fixed
branch
from
038b18b to
d873e07
Compare
Member
Author
|
I created issue #93 for extracting the theorems in |
ibbem
approved these changes
Oct 7, 2025
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 continues #85.
I implemented the operations in this PR's title and a few more. These also act as sanity checks for Indexed Sets and the proofs turned to work out like a charm.
Maybe we should consider to separate definitions and proofs (including existing proofs in
src/Vatras/Data/IndexedSet.lagda.md) by moving the proofs into asrc/Vatras/Data/IndexedSet/Properties.agdafile.