Commit 2024-05-05 19:07 7565dc2f

View on Github →

chore(Data/List): remove some long-deprecated theorems (#12350) All of these declarations have been deprecated since their files were ported (in January 2023). Move nthLe from Init to List/Basic, next to the other lemmas using it.

Estimated changes

deleted theorem List.ilast'_mem
deleted theorem List.indexOf_nthLe
added def List.nthLe
deleted theorem List.nthLe_of_eq
deleted theorem List.nthLe_zero