feat: change Array.get to take a Nat and a proof
#6032
Merged
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
kim-em
requested review from
TwoFX,
digama0,
david-christiansen,
leodemoura and
mhuisi
as code owners
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
One very minor docstring quibble. It looks like this changeset touches lots of code, and basically all of it gets nicer. That's a nice outcome! |
Co-authored-by: David Thrane Christiansen <[email protected]>
JovanGerb
pushed a commit
to JovanGerb/lean4
that referenced
this pull request
Jan 21, 2025
This PR changes the signature of `Array.get` to take a Nat and a proof, rather than a `Fin`, for consistency with the rest of the (planned) Array API. Note that because of bootstrapping issues we can't provide `get_elem_tactic` as an autoparameter for the proof. As users will mostly use the `xs[i]` notation provided by `GetElem`, this hopefully isn't a problem. We may restore `Fin` based versions, either here or downstream, as needed, but they won't be the "main" functions. --------- Co-authored-by: David Thrane Christiansen <[email protected]>
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.
This PR changes the signature of
Array.getto take a Nat and a proof, rather than aFin, for consistency with the rest of the (planned) Array API. Note that because of bootstrapping issues we can't provideget_elem_tacticas an autoparameter for the proof. As users will mostly use thexs[i]notation provided byGetElem, this hopefully isn't a problem.We may restore
Finbased versions, either here or downstream, as needed, but they won't be the "main" functions.