Commit 2024-09-08 23:21 74692d17

View on Github →

chore(List/Basic): add getElem lemmas (#16082)

  • add List.head_eq_getElem_zero;
  • add List.getElem_cons, deprecate List.get_cons;
  • add List.getElem_succ_scanl, deprecate List.get_succ_scanl;
  • use getElem lemmas for some deprecated aliases.

Estimated changes

added theorem List.getElem_cons