batteries
batteries copied to clipboard
leanprover-community
refactor: move theorems about lists from mathlib
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 [email protected]
- [x] depends-on: https://github.com/leanprover-community/batteries/pull/790
Is there a Mathlib adaptation PR ready? A lot of things are in flight at the moment so I'd like to be confident that after merging I can get everything working quickly. See e.g. what Yury did at https://github.com/leanprover/std4/pull/758.
Is there a Mathlib adaptation PR ready? A lot of things are in flight at the moment so I'd like to be confident that after merging I can get everything working quickly. See e.g. what Yury did at #758.
@semorrison I opened a Mathlib PR that removes the theorems I brought to ~~Std~~ Batteries. See https://github.com/leanprover-community/mathlib4/pull/12540.
The PR description should be a coherent summary, not a list of commit messages. If the commit messages are largely separate, then this should be separate PRs; for instance, perhaps the porting note cleanup and renames can happen in mathlib before you move things.
@eric-wieser I see. I can make separate pull requests from the later commits suggested by @semorrison. I'll do it until tomorrow. Thanks for pointing that out!
The PR description should be a coherent summary, not a list of commit messages. If the commit messages are largely separate, then this should be separate PRs; for instance, perhaps the porting note cleanup and renames can happen in mathlib before you move things.
@semorrison @eric-wieser I made a new PR from a commit and squashed the rest of the commits.