-
Notifications
You must be signed in to change notification settings - Fork 235
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
What's the 'right' notion of equality between functions? #2400
Comments
I agree that it feels inconsistent. Normally, I'd go for implicit when practice shows that it can often be inferred - but it turns out that practice is very mixed on that front! In those cases, I think going explicit is the better choice. |
I definitely vote for explicit in this case. I often run into places where it can't be inferred. |
If we make it "normal style" to use |
Since this is indeed 'intra' v2.1, I think this is the way to go. |
* fixes #2400: use explicit quantification * fix knock-ons
Closed by #2429 |
Reopening to reconsider #2381 (and possibly others?), which had previously followed Some detective work required to track them all (maybe it is just this one?) down, but in the meantime, this is perhaps a wider library design issue that we should discuss... UPDATED or else regard our agreement on explicit quantification as being library-design/style-guide worthy as a design principle? UPDATED: I think #2381 may in fact be the only outstanding inconsistency, now addressed in #2433 . Downstream [DRY] issue: refactor all of these additions (and eg UPDATED Closing now in favour of #2434 |
* fixes #2400: use explicit quantification * fix knock-ons
We have the pointwise
PropositionalEquality
definition_≗_
(moved in #2335 )and the
Function
definition_≈_
(since #2240 and its antecedent issues back to #1467 )and... we are (once again!) inconsistent as to implicit/explicit quantification.
@JacquesCarette has argued for the implicit version; @Taneb 's recent topic thread on Zulip suggests that this is not always the right choice.
Maybe there's room for both, but it doesn't feel quite right to me... or else, the distinction should be documented.
The text was updated successfully, but these errors were encountered: