batteries

batteries copied to clipboard

This test is timing-sensitive, and has [spuriously failed](https://github.com/leanprover-community/batteries/actions/runs/10036728715/job/27735044947?pr=887) before. Increase the timings slightly to make it less easy to race.

digama0

feat: statically sized Vector type

17

This PR adds a static vector type to batteries akin to `Mathlib.Data.Vector` with a key difference: It is based on `Array` instead of `List` and is designed for efficient operations...

Shreyas4991

This is a follow-up to #849 which uses #793 to simplify major parts of the code, paving the way toward correctness proofs for `BinaryHeap`. - [x] Depends on #849 -...

fgdorais

feat: order lemmas for `UIntX` types

2

fgdorais

feat: Add `String.isPrefixOf` theorems

1

This PR is a redo of #782, but adds the following: - Auxiliary theorems used to prove the theorems below - These were already in #782 - Proof of equivalence...

tjf801

refactor: avoid relying on rfl's behavior on ground terms

4

`rfl` for ground terms will reduce at transparency `.all`, even if the current transparency is `.default`. Maybe it's prudent to not rely on this corner case, and have more explicit...

nomeata

- [ ] Depends on #813 - [x] Depends on #814 - [x] Depends on #827

fgdorais

chore: upstream `Nat.binaryRec`

3

Since upstreaming to core (https://github.com/leanprover/lean4/pull/3756) is still controversial, I'd like it to be upstreamed to Batteries first. - [x] Depends on: leanprover-community/mathlib4#19666

astrainfinita

kim-em

fgdorais