batteries

batteries copied to clipboard

feat: add `Fin.sum`, `Fin.prod`, `Fin.count`

5

fgdorais

feat: add stream combinators

1

- [ ] Depends on #1331 This PR adds basic combinators for stream types.

fgdorais

feat: add finite and well-founded streams

3

Add classes for provably finite streams and connect streams with standard library iterators.

fgdorais

Similarly to how syntax linters in Lean core do it: https://github.com/leanprover/lean4/blob/206eb73cd9de4b58abbb2eae20a41fd9b7af187b/src/Lean/Linter/Basic.lean#L75 The relevant code seems to be at: https://github.com/leanprover-community/batteries/blob/6f7d05f4955eb5af9799d828b697251bb2c9c0b8/Batteries/Tactic/Lint/Frontend.lean#L194 cf. [#FLT > unused argument linter issue @ 💬](https://leanprover.zulipchat.com/#narrow/channel/416277-FLT/topic/unused.20argument.20linter.20issue/near/543106977) (It might...

bryangingechen

Mathlib's BigOperators library is well-developed, sophisticated and works extremely well. There is however a need for a less sophisticated intermediate library built directly on Std's basic classes for associativity, commutativity,...

fgdorais

Verify Binary Heap

4

This is a standard textbook algorithm. It is well implemented in [Batteries.Data.BinaryHeap](https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/BinaryHeap.lean) but not verified. If you're looking to get started with formal verification project in Lean, this should be...

fgdorais

feat: add `Nat.Digits`

3

This PR adds functions for calculating digit representation in any base. Both little-endian and big-endian versions are provided.

fgdorais

I am not sure if this is ultimately a mathlib or batteries issue but I have been advised to post this here. See the discussion at the end of https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Chain.20and.20Chain'.20and.20Pairwise/with/540902002...

linesthatinterlace

This adds the `Monad m` arguments needed after https://github.com/leanprover/lean4/pull/10204

eric-wieser

feat: fix some issues with `equals t => tac`

2

This PR fixed some issues with the `conv` tactic `equals t => tac`: - It gives bad error messages when `t` has the wrong type. For example, ``` type mismatch...

plp127