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
toList.get_cyclicPermutations
. While the old lemma wasn't deprecated during port, the definitionList.nthLe
was, so I think that we can drop the lemma without a deprecation period.