Commit 2025-11-09 23:02 4e1b0760

View on Github →

chore: adaptations for batteries#1503 (#31422) After [batteries#1503](https://github.com/leanprover-community/batteries/pull/1503) is merged:

  • Edit the lakefile to point to leanprover-community/batteries:main
  • Run lake update batteries
  • Merge leanprover-community/mathlib4:master
  • Wait for CI and merge

Estimated changes

deleted theorem List.drop_scanr
deleted theorem List.getElem?_scanl_zero
deleted theorem List.getElem?_scanr
deleted theorem List.getElem?_scanr_of_lt
deleted theorem List.getElem?_scanr_zero
deleted theorem List.getElem?_succ_scanl
deleted theorem List.getElem_scanl_zero
deleted theorem List.getElem_scanr
deleted theorem List.getElem_scanr_zero
deleted theorem List.getElem_succ_scanl
deleted theorem List.head_scanl
deleted theorem List.head_scanr
deleted theorem List.length_scanl
deleted theorem List.length_scanr
deleted theorem List.scanl_cons
deleted theorem List.scanl_iff_nil
deleted theorem List.scanl_ne_nil
deleted theorem List.scanl_nil
deleted theorem List.scanr_append
deleted theorem List.scanr_cons
deleted theorem List.scanr_iff_nil
deleted theorem List.scanr_ne_nil
deleted theorem List.scanr_nil
deleted theorem List.tail_scanr