feat: add String.splitOn_of_valid
#719
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
WIP |
chabulhwi
force-pushed
the
String.splitOn_of_valid_v2
branch
6 times, most recently
from
38dadf0 to
bd4c1fe
Compare
leanprover-community-mathlib4-bot
added
the
merge-conflict
chabulhwi
force-pushed
the
String.splitOn_of_valid_v2
branch
2 times, most recently
from
ff8f99b to
7f41b9a
Compare
|
Since the current definition of |
chabulhwi
force-pushed
the
String.splitOn_of_valid_v2
branch
2 times, most recently
from
059c653 to
fd15c80
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Move the theorem from `Mathlib.Logic.Function.Basic` to Std.
Move theorems about lists from `Mathlib.Data.List.Basic` to Std. I removed the `nolint` attribute from `List.modifyHead_modifyHead`.
Move the theorem from `Mathlib.Data.List.Infix` to Std.
* `List.splitOnceP` returns `(l₁, l₂)` for the first split `l = l₁ ++ l₂` such that `P l₂` returns true. * `List.splitOnList` splits a list at every occurrence of a separator list. The separators are not in the result. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
chabulhwi
force-pushed
the
String.splitOn_of_valid_v2
branch
from
fd15c80 to
da03911
Compare
|
Since leanprover/lean4#3829 was fixed, I'll make a third version of #495. |
2 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
refactor: move
Function.id_deffrom mathlibMove the theorem from
Mathlib.Logic.Function.Basicto Std.refactor: move theorems about lists from mathlib
Mathlib.Data.List.Basicto Std.nolintattribute fromList.modifyHead_modifyHead.refactor: move
List.cons_prefix_ifffrom mathlibMove the theorem from
Mathlib.Data.List.Infixto Std.feat: add lemmas about lists
feat: add
Std.Data.List.SplitOnListList.splitOncePreturns(l₁, l₂)for the first splitl = l₁ ++ l₂such thatP l₂returns true.List.splitOnListsplits a list at every occurrence of a separator list. The separators are not in the result.Co-authored-by: Mario Carneiro di.gama@gmail.com
Co-authored-by: Scott Morrison scott.morrison@gmail.com
feat: add lemmas about
Nat.addfeat: add
String.splitOn_of_validThis is the second version of #495 and includes #531.