-
Notifications
You must be signed in to change notification settings - Fork 316
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
Clean up quotient APIs #16210
base: master
Are you sure you want to change the base?
Clean up quotient APIs #16210
Conversation
PR summary aa203fbe8cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
!bench |
Here are the benchmark results for commit c0d07be. |
!bench |
Here are the benchmark results for commit 4ae7e83. |
We may migrate toQuot
andIsEquiv
APIs in the future, but it might be a good start to clean upQuotient
APIs anyway.The diffs in this PR did not include
QuotLike
APIs, but eventually I decided to migrate toQuotLike
before deprecating the old APIs. See Zulip.Setoid
#16254[s : Setoid α]
=>{s : Setoid α}
#16256Setoid.r
#16258Setoid.Rel
#16260Quotient.mk''
an abbrev ofQuotient.mk _
#16264[s : Setoid α]
=>{s : Setoid α}
#16267surjective_*_mk
=>*.surjective_mk
#16410[s : Setoid α]
=>{s : Setoid α}
#17588QuotLike
QuotLike
#16421QuotLike
APIs #16428Deprecating
ind*'
APIs #16314liftOn'
APIs #16414remaining diffs