-
Notifications
You must be signed in to change notification settings - Fork 298
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
[Merged by Bors] - feat(data/{sym2,sym}) decidable version of sym2.mem.other, filling out some of sym API #4008
Conversation
Removes `sym2.vmem` and replaces it with `sym2.mem.other'`, which can get the other element of a pair in the presence of decidable equality. Writing `sym2.mem.other'` was beyond my abilities when I created `sym2.vmem`, and seeing that vmem is extremely specialized and has no immediate use, it's probably best to remove it. Adds some assorted simp lemmas, and also an additional lemma that `sym2.mem.other` is, in some sense, an involution. Adds to the API for `sym`. This is from taking some of the interface for multisets. (This was from exploring whether `sym2 α` should be re-implemented as `sym α 2` and trying to add enough to `sym` to pull it off, but it doesn't seem to be worth it.) (I'm not committing a recursor for `sym α n`, which lets you represent elements as vectors of length `n`. It needs some cleanup.)
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.
Apart from Scott's request, this looks quite good to me. @kmill let's get this merged?!
@jcommelin Fixed the import line (didn't mean to revert @semorrison's cleanup!) |
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.
Thanks 🎉
bors merge
…t some of sym API (#4008) Removes `sym2.vmem` and replaces it with `sym2.mem.other'`, which can get the other element of a pair in the presence of decidable equality. Writing `sym2.mem.other'` was beyond my abilities when I created `sym2.vmem`, and seeing that vmem is extremely specialized and has no immediate use, it's probably best to remove it. Adds some assorted simp lemmas, and also an additional lemma that `sym2.mem.other` is, in some sense, an involution. Adds to the API for `sym`. This is from taking some of the interface for multisets. (I was exploring whether `sym2 α` should be re-implemented as `sym α 2` and trying to add enough to `sym` to pull it off, but it doesn't seem to be worth it in the end.) (I'm not committing a recursor for `sym α n`, which lets you represent elements by vectors of length `n`. It needs some cleanup.)
Pull request successfully merged into master. Build succeeded: |
Removes
sym2.vmem
and replaces it withsym2.mem.other'
, which can get the other element of a pair in the presence of decidable equality. Writingsym2.mem.other'
was beyond my abilities when I createdsym2.vmem
, and seeing that vmem is extremely specialized and has no immediate use, it's probably best to remove it.Adds some assorted simp lemmas, and also an additional lemma that
sym2.mem.other
is, in some sense, an involution.Adds to the API for
sym
. This is from taking some of the interface for multisets. (I was exploring whethersym2 α
should be re-implemented assym α 2
and trying to add enough tosym
to pull it off, but it doesn't seem to be worth it in the end.)(I'm not committing a recursor for
sym α n
, which lets you represent elements by vectors of lengthn
. It needs some cleanup.)