Commit 2023-11-07 10:14 b792832d

View on Github →

chore: rename List.rdrop to dropRight (#8233)

<!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] -->

Open in
Gitpod

Estimated changes

deleted theorem List.dropWhile_idempotent
deleted theorem List.mem_rtakeWhile_imp
deleted def List.rdrop
deleted def List.rdropWhile
deleted theorem List.rdropWhile_concat
deleted theorem List.rdropWhile_last_not
deleted theorem List.rdropWhile_nil
deleted theorem List.rdropWhile_prefix
deleted theorem List.rdropWhile_singleton
deleted theorem List.rdrop_concat_succ
deleted theorem List.rdrop_nil
deleted theorem List.rdrop_zero
deleted def List.rtake
deleted def List.rtakeWhile
deleted theorem List.rtakeWhile_concat
deleted theorem List.rtakeWhile_nil
deleted theorem List.rtakeWhile_suffix
deleted theorem List.rtake_concat_succ
deleted theorem List.rtake_nil
deleted theorem List.rtake_zero