batteries

batteries copied to clipboard

It was still present in the namespaces `Std.Tactic.Lint` and `Std.CodeAction`.

digama0

feat: add finRange

2

This is to correct a name clash from #528 with Mathlib pointed out by @eric-wieser We add `List.finRange` and `Array.finRange` (with basic lemmas). The synonyms `Fin.list` and `Fin.enum` are deprecated.

fgdorais

These have been recently requested on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regarding.20map.20and.20extract.20for.20Byte.2FFloatArrays/near/452971124).

fgdorais

fgdorais

fgdorais

feat: `Fin.foldlM` and `Fin.foldrM`

3

- [x] Depends on #827

fgdorais

feat: add `ByteSubarray`

1

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`...

fgdorais

feat: size lemma for `Array.set!`

1

fgdorais

General purpose bisection algorithm.

fgdorais

These were previously moved to core (verbatim) in leanprover/lean4#3290.

digama0