Commit 2024-04-24 12:37 7aace659

View on Github →

feat(List/rotate): migrate to get, new lemmas, golf (#12171)

  • Add List.Nodup.rotate_congr_iff, List.cyclicPermutations_ne_nil, List.head?_cyclicPermutations, List.head_cyclicPermutations, List.cyclicPermutations_injective, List.cyclicPermutations_inj.
  • Change List.nthLe_cyclicPermutations to List.get_cyclicPermutations. While the old lemma wasn't deprecated during port, the definition List.nthLe was, so I think that we can drop the lemma without a deprecation period.

Estimated changes