Commit 2024-08-12 02:13 e5d297f0

View on Github →

chore(*): use getElem instead of List.get/List.nthLe (#15455) Deletions:

  • List.toFinsupp_apply_lt'

Estimated changes

added theorem List.erase_getElem
modified theorem List.getD_eq_get
added theorem List.getD_eq_getElem
added theorem List.getI_eq_getElem
modified theorem List.toFinsupp_apply_fin
deleted theorem List.toFinsupp_apply_lt'
modified theorem List.toFinsupp_apply_lt