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: stronger proof strategy for partial inhabitation #5847

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

feat: stronger proof strategy for partial inhabitation #5847

wants to merge 4 commits into from

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Oct 26, 2024 •
edited
Loading

Now partial will try to extract more inhabitants of types by trying to find inhabitants of arguments' arguments.

For example, in a callback-based function like

partial def withCallback (k : Array Nat → IO α) : IO α := ...

it can see that Array Nat is inhabited, so from k it gets an inhabitant of IO α.

@kmill
feat: stronger proof strategy for partial inhabitation
9be0817 
Now `partial` will try to extract more inhabitants of types by trying to find inhabitants of arguments' arguments.

For example, in a callback like
```lean
partial def withCallback (k : Array Nat → IO α) : IO α := ...
```
it can see that `Array Nat` is inhabited, so with `k` it gets an inhabitant of `IO α`.
@kmill kmill added the awaiting-review Waiting for someone to review the PR label Oct 26, 2024
@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 Oct 26, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 26, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5847
79b41de
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 26, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5847
9f5b774
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 26, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-5847 has successfully built against this PR. (2024-10-26 01:45:13) View Log
  • ✅ Mathlib branch lean-pr-testing-5847 has successfully built against this PR. (2024-10-26 17:36:04) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c3cbc92a0c79c1c20b59251c9799371a4b9bf11d --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-30 20:47:30)

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 26, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5847
8e3983c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5847
d771353
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
awaiting-review Waiting for someone to review the PR 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
Projects
None yet
Milestone
No milestone
Development

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