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/univariate/qpf): compositional data type framework for (co)inductive types #3325
Conversation
…inductive types single out univariate qpfs
The definition itself is similar. We format the arguments differently because we it as part of an F-algebra. I can't see any function that we have in common. Sharing the definition of |
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.
Module doc strings still need to be added everywhere.
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
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.
Remaining stylistic issues aside, this looks good to me.
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
I wonder if I should move |
That's a good idea. |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
…inductive types (leanprover-community#3325) Define univariate QPFs (quotients of polynomial functors). This is the first part of leanprover-community#3317.
Define univariate QPFs (quotients of polynomial functors). This is the first part of #3317.