[Merged by Bors] - fix(logic/basic): remove noncomputable lemma
#10292
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
changed the title
noncomputable lemmanoncomputable lemma
eric-wieser
added
the
awaiting-review
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Nov 15, 2021
It's been three years since this was discussed according to the zulip archive link in the library note. According to CI, the reason is no longer relevant. Leaving these as `noncomputable lemma` is harmful as it results in non-defeq instance diamonds sometimes as lean was not able to unfold the lemmas to get to the data underneath. Since these are now `def`s, the linter requires them to have docstrings.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
noncomputable lemmanoncomputable lemma
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
It's been three years since this was discussed according to the zulip archive link in the library note.
According to CI, the reason is no longer relevant. Leaving these as
noncomputable lemmais harmful as it results in non-defeq instance diamonds sometimes as lean was not able to unfold the lemmas to get to the data underneath.Since these are now
defs, the linter requires them to have docstrings.This came up on Zulip.