Commit 2024-04-30 07:19 335470e5

View on Github →

chore(List): delete old, unused, deprecated theorems (#9607) These theorems have been deprecated for at least a year, and are unused.

Estimated changes

deleted theorem List.cons_nthLe_drop_succ
deleted theorem List.get?_eq_some'
deleted theorem List.getLast_eq_nthLe
deleted theorem List.nthLe_append
deleted theorem List.nthLe_drop'
deleted theorem List.nthLe_drop
deleted theorem List.nthLe_eq_iff
deleted theorem List.nthLe_length_sub_one
deleted theorem List.nthLe_replicate
deleted theorem List.nthLe_set_eq
deleted theorem List.nthLe_set_of_ne
deleted theorem List.nthLe_take'
deleted theorem List.nthLe_take
deleted theorem List.some_nthLe_eq