Skip to content
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

chore(*): bundle typeclasses #18775

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

chore(*): bundle typeclasses #18775

wants to merge 2 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Apr 9, 2023

For instance, [is_trans α r] [is_antisymm α r] [is_total α r][is_linear_order α r]. They're mathematically equivalent, but the latter is more concise and allows access to more instances.

This isn't exhaustive.


Open in Gitpod

@vihdzp vihdzp added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 9, 2023
@vihdzp vihdzp added the t-order Order hierarchy label Apr 9, 2023
@eric-wieser
Copy link
Member

but the latter [...] allows access to more instances.

This isn't true, is it? The less bundled spelling is implied by the more bundled, so the former is more general to have in variables statements.

@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR t-order Order hierarchy too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants