batteries

batteries copied to clipboard

feat: add `String.splitOn_of_valid`

8

`String.splitOn_of_valid` is the first of the eleven unproved theorems about strings. I added the following to prove it: * lemmas about `Nat.add` and lists * the file `Batteries.Data.List.SplitOnList` * the...

chabulhwi

refactor: move theorems about lists from mathlib

9

`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. We need these theorems to prove `String.splitOn_of_valid`. See https://github.com/leanprover-community/batteries/pull/743. Batteries bump PR in Mathlib: https://github.com/leanprover-community/mathlib4/pull/12540 Co-authored-by: Kim Morrison --- - [x] depends-on: https://github.com/leanprover-community/batteries/pull/790

chabulhwi

kim-em

This is an attempt to switch to using `lake test`. Gradually more of this functionality will be taken over by `lake`, but I would like to push this along and...

kim-em

kim-em

- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 This adds `RBSet.upperBound?` symmetric to `lowerBound?`, and lifts all the RBNode theorems to RBSet (and...

digama0

Add some theorems for `String.substrEq` and `String.isPrefixOf`

1

tjf801

feat: Add `String.length_join` and `List.length_join`

3

Quick fix for #770.

tjf801

TwoFX

This adds an implementation of exact (IEEE conforming) rounding from `Rat` to `Float` rounding nearest ties to even. Note that unlike most other lean functions (but like most float functions),...

digama0