Commit 2024-10-21 03:20 4d87f692

View on Github →

chore: rename List.modifyNth->modify and insertNth->insertIdx (#17985) This relies on a branch of Batteries, so needs a delegation not a merge. See zulip discussion.

Estimated changes

deleted theorem List.modifyNth_eq_set
added theorem List.modify_eq_set
added theorem List.insertIdx_comm
added theorem List.insertIdx_zero
added theorem List.length_insertIdx
added theorem List.mem_insertIdx
deleted theorem List.eraseIdx_insertNth
deleted theorem List.get_insertNth_of_lt
deleted theorem List.get_insertNth_self
deleted theorem List.insertNth_comm
deleted theorem List.insertNth_injective
deleted theorem List.insertNth_succ_cons
deleted theorem List.insertNth_succ_nil
deleted theorem List.insertNth_zero
deleted theorem List.length_insertNth
deleted theorem List.mem_insertNth
deleted theorem List.continuous_insertNth
added theorem List.tendsto_insertIdx
deleted theorem List.tendsto_insertNth'
deleted theorem List.tendsto_insertNth
deleted theorem Vector.tendsto_insertNth