Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

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.

@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
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.

3 participants