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

chore: upstream IsPrefix/IsSuffix/IsInfix #4836

Merged
merged 1 commit into from
Jul 26, 2024
Merged

chore: upstream IsPrefix/IsSuffix/IsInfix #4836

merged 1 commit into from
Jul 26, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Jul 26, 2024

Further lemmas to follow; this is the basic material from Batteries.

@kim-em kim-em requested a review from digama0 as a code owner July 26, 2024 04:18
@kim-em kim-em enabled auto-merge July 26, 2024 04:18
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 26, 2024 04:30 Inactive
@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 Jul 26, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54c22efca1cb6fdcea694b894ca9830d0b5c4b0e --onto 39e0b41fe1ab4d16f15efb0dc9bd7607a8941713. (2024-07-26 04:34:31)

@kim-em kim-em added this pull request to the merge queue Jul 26, 2024
Merged via the queue into master with commit 8c87a90 Jul 26, 2024
13 checks passed
@zhassan-aws zhassan-aws mentioned this pull request Aug 12, 2024
Merged
BrunoDutertre pushed a commit to model-checking/rust-lean-models that referenced this pull request Aug 13, 2024
@zhassan-aws
Remove mathlib dependency (#9)
bc90fc7 
Remove mathlib from dependencies and fix all proofs.

Call outs: I had to add `batteries` as a dependency, but all
definitions/theorems needed from `batteries` (e.g. `List.IsPrefix`) have
been upstreamed in
https://github.com/leanprover/lean4/releases/tag/v4.11.0-rc1 (e.g.
leanprover/lean4#4836), so we should be able to
get rid of the `batteries` dependency as well once v4.11.0 is released.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees
No one assigned
Labels
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.
2 participants
@kim-em @leanprover-community-mathlib4-bot