Commit 2025-02-21 10:58 b0e9db7e

View on Github →

chore: backport changes to getElem lemmas (#22146) These changes are backports from bump/nightly-2025-02-20.

Estimated changes

deleted theorem List.ext_get?'
deleted theorem List.ext_get?_iff'
deleted theorem List.ext_get?_iff
added theorem List.ext_getElem?'
added theorem List.ext_getElem?_iff'
modified theorem List.foldr_eta
deleted theorem List.get_eq_get?
added theorem List.get_eq_getElem?
deleted theorem List.idxOf_get?
deleted theorem List.next_get
added theorem List.next_getElem
deleted theorem List.prev_get
added theorem List.prev_getElem
deleted theorem List.getD_eq_getD_get?
deleted theorem List.getI_eq_iget_get?
deleted theorem List.get?_ofFn
deleted theorem List.get?_succ_scanl
deleted theorem List.get?_zipWith'
deleted theorem List.get?_zipWith_eq_some
deleted theorem List.get?_zip_eq_some
deleted theorem Set.range_list_get?