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: automatic attach introduction in well-founded recursion #6744

Draft
wants to merge 16 commits into
base: nightly-with-mathlib
Choose a base branch
from
Draft

feat: automatic attach introduction in well-founded recursion #6744

wants to merge 16 commits into from
+171,923 −118,270

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Jan 22, 2025

(Early exploratory WIP.)

@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 22, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6744
9030431
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6744
1dec0bf
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 22, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 22, 2025 •
edited
Loading

Mathlib CI status (docs):

@nomeata nomeata changed the base branch from master to nightly-with-mathlib January 23, 2025 10:32
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jan 23, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 23, 2025 10:49 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6744
05276df
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6744
9704951
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 23, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 23, 2025 14:22 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6744
9013470
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6744
0093fee
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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
@nomeata @leanprover-community-bot