chore: rename fields of Subarray to follow Lean conventions #3851
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Co-authored-by: Eric Wieser <[email protected]>
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
| h₁ : start ≤ stop | ||
| h₂ : stop ≤ as.size | ||
| start_le_stop : start ≤ stop | ||
| stop_le_array_size : stop ≤ array.size |
There was a problem hiding this comment.
| stop_le_array_size : stop ≤ array.size | |
| stop_le_size : stop ≤ array.size |
this still seems sufficiently precise/descriptive and is less annoyingly long
There was a problem hiding this comment.
Ha, that's what I originally had! I changed it because Subarray.size exists with a different meaning.
I'll hold off on the merge for a short bit and think it over a second time.
There was a problem hiding this comment.
Oh, yeah that is awkward. I wonder if we could change the name to avoid confusion (i.e. Subarray.length)? I think we will want names for both of these quantities eventually (e.g. in lemmas), so it would be good to think about what names are clear and distinct. length and size? size and fullSize? extent and maxStop? Or just use t.array.size.
As a pedantic note, prefix naming convention would yield stop_le_size_array.
There was a problem hiding this comment.
On reflection, I expect that this projection will not be used so often (mostly I expect users to be using the API here, or writing meaningful operators that preserve the invariants - borne out by the very small changes needed for Std and Aesop and the fact that Mathlib itself needed none), so I'll go with explicitness over concision.
Thanks!
|
OK, Mathlib builds against leanprover-community/batteries#733 and leanprover-community/aesop#122 locally for me. |
|
Closes #2164 |
No description provided.