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: functional induction for mutual structural recursion #4772

Merged
merged 56 commits into from
Jul 22, 2024
Merged

feat: functional induction for mutual structural recursion #4772

merged 56 commits into from
Jul 22, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Jul 17, 2024

No description provided.

@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 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jul 17, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-17 10:18:00)
  • ✅ Mathlib branch lean-pr-testing-4772 has successfully built against this PR. (2024-07-18 09:23:44) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 204d4839fadf099347b255f95916759bbd8d90dc --onto a94805ff71f7576ee014aafc76b29e29b066bd80. (2024-07-19 15:08:37)
  • ✅ Mathlib branch lean-pr-testing-4772 has successfully built against this PR. (2024-07-21 14:03:46) View Log
  • ✅ Mathlib branch lean-pr-testing-4772 has successfully built against this PR. (2024-07-21 15:50:30) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 22ae04f3e7ea716c4af5cfbab587370d10cc06fa --onto 8ceb24a5e6782aac39fdb3bb2b47021ac38d0847. (2024-07-22 07:45:22)
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-22 08:39:59)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-22 10:46:55)
  • 🟡 Mathlib branch lean-pr-testing-4772 build against this PR was cancelled. (2024-07-22 12:02:51) View Log
  • ✅ Mathlib branch lean-pr-testing-4772 has successfully built against this PR. (2024-07-22 12:57:40) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3a4d2cded30beb3343ba0e13a3ddb2809703e26d --onto 22ae04f3e7ea716c4af5cfbab587370d10cc06fa. (2024-07-22 15:12:03)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 18, 2024 08:14 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 18, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4772
1ddd63a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 18, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4772
8f26c3d
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 18, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 18, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
c299f88
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 18, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
2a315fe
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 22, 2024 08:32 Inactive
@nomeata nomeata marked this pull request as ready for review July 22, 2024 09:16
@nomeata nomeata requested a review from leodemoura as a code owner July 22, 2024 09:16
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Jul 22, 2024
nomeata added 7 commits July 22, 2024 12:33
@nomeata
Introduce PProdN module, replace FunPacker module
edd1a81
@nomeata
refactor: Introduce PProdN module
3eb412e 
code to create nested `PProd`s, and project out, and related functions
were scattered in variuos places. This unifies them in
`Lean.Meta.PProdN`.

It also consistently avoids the terminal `True` or `PUnit`, for slightly
easier to read constructions.
@nomeata
Merge branch 'joachim/pprodn' into joachim/funind-structural-mutual
1ea9013
@nomeata
Update tests
a70c0ef
@nomeata
Merge branch 'joachim/pprodn' into joachim/funind-structural-mutual
0d8acf5
@nomeata
More test updates
294499b
@nomeata
Merge branch 'joachim/pprodn' into joachim/funind-structural-mutual
8d657bf
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 22, 2024 11:06 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
5f6d55f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
74c2603
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 22, 2024 11:51 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
959d5ba
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4772
f808e4d
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 22, 2024 13:06 Inactive
@nomeata nomeata enabled auto-merge July 22, 2024 14:58
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 22, 2024 15:04 Inactive
@nomeata nomeata added this pull request to the merge queue Jul 22, 2024
Merged via the queue into master with commit 9f1eb47 Jul 22, 2024
13 checks passed
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 is a code owner

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