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: containsThenInsert for the tree map #6857

Draft
wants to merge 42 commits into
base: paul/treemap1b
Choose a base branch
from
Draft

feat: containsThenInsert for the tree map #6857

wants to merge 42 commits into from

Conversation

datokrat
Copy link
Contributor

This PR introduces the containsThenInsert function on the tree maps of the standard library.

datokrat added 30 commits January 22, 2025 17:00
@datokrat
copy
aab0b5b
@datokrat
wip
e65d67c
@datokrat
add prelude declarations
2a41b4a
@datokrat
move Associative
042ebde
@datokrat
Merge remote-tracking branch 'origin/master' into paul/treemap1a
63ea5d4
@datokrat
provide docstrings
5ad9155
@datokrat
cleanup
ac56230
@datokrat
remove debug option
1d5965c
@datokrat
add prelude declarations
7f8ddbc
@datokrat
prepare bootstrapping
98812e1
@datokrat
chore: update stage0
4b7f12e
@datokrat
chore: update stage0
bf0ab26
@datokrat
chore: update stage0
c05d4e8
@datokrat
chore: update stage0
71c014d
@datokrat
chore: update stage0
6d045c3
@datokrat
revert stage0
0d7bd56
@datokrat
chore: update stage0
be42ee2
@datokrat
revert stage0
a175175
@datokrat
chore: update stage0
6094b49
@datokrat
revert stage0
85295cd
@datokrat
chore: update stage0
b17ccb0
@datokrat
revert stage0
8e25e86
@datokrat
chore: update stage0
ef2acd9
@datokrat
wip
c6989c1
@datokrat
chore: update stage0
d253387
@datokrat
wip
c2f1a2c
@datokrat
cleanups
85b44f6
@datokrat
cleanups
423b640
@datokrat
extract Ord lemmas
591c1c2
@datokrat
refactor classes and repair imports of deleted files
6243911
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jan 29, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 29, 2025 20:11 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 Jan 29, 2025
@leanprover-community-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 c073da20ce2d30b2df6436852fd229a5eae7b323 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 20:27:08)

@datokrat datokrat changed the base branch from master to paul/treemap1b January 30, 2025 08:05
@datokrat datokrat force-pushed the paul/treemap1b branch 2 times, most recently from 9a611a8 to 008ce54 Compare February 11, 2025 15:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX will be requested when the pull request is marked ready for review TwoFX is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees
No one assigned
Labels
changes-stage0 Contains stage0 changes, merge manually using rebase 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
@datokrat @leanprover-community-bot