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: partial_fixpoint: theory #6477

Merged
merged 2 commits into from
Jan 2, 2025
Merged

feat: partial_fixpoint: theory #6477

merged 2 commits into from
Jan 2, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Dec 30, 2024

This PR adds the necessary domain theory that backs the
partial_fixpoint feature.

Part of #6355.

@nomeata
feat: partial_fixpoint: theory
3a5f0e6 
This PR adds the necessary domain theory that backs the
`partial_fixpoint` feature.

Part of #6355.
@nomeata nomeata added will-merge-soon …unless someone speaks up changelog-library Library labels Dec 30, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 30, 2024 11:03 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 Dec 30, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6477
d30c27a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6477
5bfc65b
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 30, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 30, 2024 •
edited
Loading

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 30, 2024 12:07 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 30, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6477
3805e4a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6477
17cff69
@nomeata nomeata added this pull request to the merge queue Jan 2, 2025
Merged via the queue into master with commit 7d0c0d4 Jan 2, 2025
19 checks passed
@nomeata nomeata deleted the joachim/partial_fixpoint_theory branch January 2, 2025 11:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-bot