Commit 2024-10-14 07:22 81429386

View on Github →

refactor: move theorem about lists to batteries (#12540) List.modifyHead_modifyHead is from Mathlib.Data.List.Basic. I need it to prove String.splitOn_of_valid. See https://github.com/leanprover-community/batteries/pull/743. Corresponding Batteries PR: https://github.com/leanprover-community/batteries/pull/756

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.modifyHead_modifyHead

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.subperm_nil

Modified lake-manifest.json