Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add lemmas about List.IsPrefix #5448

Merged
merged 5 commits into from
Sep 26, 2024
Merged

feat: add lemmas about List.IsPrefix #5448

merged 5 commits into from
Sep 26, 2024

Conversation

Command-Master
Copy link
Contributor

@Command-Master Command-Master commented Sep 24, 2024 •
edited
Loading

Add iff version of List.IsPrefix.getElem, and eq_of_length_le variants of List.IsInfix.eq_of_length, List.IsPrefix.eq_of_length, List.IsSuffix.eq_of_length

@Command-Master
Copy link
Contributor Author

WIP

@github-actions github-actions bot added the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Sep 24, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 24, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Sep 24, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3190be30589a36c3e8b2be9d49a046702ce37692 --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-24 05:04:20)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3190be30589a36c3e8b2be9d49a046702ce37692 --onto 7845a05cf1094f24a5c4a51c32dd84bf4ff31a54. (2024-09-26 04:26:45)

@Command-Master
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. labels Sep 24, 2024
@kim-em kim-em marked this pull request as ready for review September 26, 2024 03:12
@kim-em
Copy link
Collaborator

kim-em commented Sep 26, 2024

Thanks! Minor change requested, but otherwise LGTM.

@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Sep 26, 2024
@Command-Master
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Sep 26, 2024
@kim-em kim-em added this pull request to the merge queue Sep 26, 2024
Merged via the queue into leanprover:master with commit 3d1ac7c Sep 26, 2024
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Command-Master @leanprover-community-mathlib4-bot @kim-em