feat: add `ByteSubarray`

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

242 stars 101 forks source link

feat: add `ByteSubarray` #851

Closed fgdorais closed 2 months ago

fgdorais commented 4 months ago

Alternative to #836. While this is not quite a drop-in replacement for users of Mathlib's ByteSlice, it offers the same functionality while using the same basic structure as core's Subarray type.

This fixes the issues I raised in #836 but I'm also happy with compromises. For example, I personally think ByteSlice is a better name than ByteSubarray. I'm also a fan of the offset/length approach but this seems to much of a divergence from Subarray.

kim-em commented 2 months ago

I have no particular opinion here (as I don't know of any use cases yet), but I will happily deprecate Mathlib's ByteArray in favour of this when it is merged.