Closed
Conversation
Member
|
Could you check that you have all the lemmas from Mathlib, and that the names and statements match? |
Collaborator
Author
|
It's not my aim to get all the lemmas from Mathlib, but the names for the few that are here do agree. Are there any specific lemmas from Mathlib that you think are missing? |
eric-wieser
reviewed
Aug 1, 2024
| | l, [], t => reverseAux t l | ||
| | a::l, b::r, t => bif s a b then loop l (b::r) (a::t) else loop (a::l) r (b::t) | ||
|
|
||
| /-- `finRange n` is the list of all elements of `Fin n` in order -/ |
Member
There was a problem hiding this comment.
In mathlib the docstring is
/-- All elements of `Fin n`, from `0` to `n-1`. The corresponding finset is `Finset.univ`. -/
Should the last sentence be kept, with an added "in mathlib"?
Collaborator
Author
There was a problem hiding this comment.
Good question. I'm not sure. How useful is the second sentence for Mathlib users? It seems like it is a trivial conclusion from the first sentence, isn't it? (Provided one knows what Finset is.)
Collaborator
Author
|
Closing for now since this will require substantial revisions after #956 gets merged. |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This is to correct a name clash from #528 with Mathlib pointed out by @eric-wieser
We add
List.finRangeandArray.finRange(with basic lemmas). The synonymsFin.listandFin.enumare deprecated.