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/list/to_finsupp): computable finsupp from list #15161
Conversation
Also prove some things about `list.inth` on the way. On the way to computable list-based polynomials
Fill out some of the `enum` and `enum_from` API Link the two via `map_fst_add_enum_eq_enum_from`.
With some additional API for pairwise on multisets and coerced lists On the way to computable list-based polynomials
via `list.nthd`
…nto pechersky/list-to-finsupp
…chersky/list-to-finsupp
If we're truly after computability for polynomials, could we just define them with dfinsupp? |
Do you mean change the underlying implementation for |
It is no longer a simp lemma
`nth_eq_nth_le` doesn't have `simp` either.
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
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.
LGTM otherwise.
bors d+
✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
via `list.nthd` On the way to computable list-based polynomials Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
via `list.nthd` On the way to computable list-based polynomials Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
via
list.nthd
On the way to computable list-based polynomials