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: basic support for handling enum inductives in bv_decide #6946

Merged
merged 4 commits into from
Feb 10, 2025
Merged

feat: basic support for handling enum inductives in bv_decide #6946

merged 4 commits into from
Feb 10, 2025

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Feb 4, 2025 •
edited
Loading

This PR implements basic support for handling of enum inductives in bv_decide. It now supports equality on enum inductive variables (or other uninterpreted atoms) and constants.

@hargoniX hargoniX added the changelog-language Language features, tactics, and metaprograms label Feb 4, 2025
@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 Feb 4, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 4, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-02-04 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. (2025-02-04 10:09:27)
  • ✅ Mathlib branch lean-pr-testing-6946 has successfully built against this PR. (2025-02-04 11:41:34) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 897e9c5388a139ac24069da6e6978ee60f914039 --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-05 15:52:43)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 947cd742bf7dd1c2ca961bd464960779d2bdcd39 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-06 11:09:35)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4540a6436f3bee95dcaa3c746b738aa014ff41d8 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-06 12:14:25)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-02-10 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. (2025-02-10 10:04:29)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 4, 2025 10:43 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6946
b6eebf2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6946
8bcc156
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 4, 2025
@hargoniX hargoniX force-pushed the hbv/bv_decide_enums branch 3 times, most recently from 8181afc to 571d882 Compare February 6, 2025 10:41
@hargoniX hargoniX mentioned this pull request Feb 6, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Feb 6, 2025
@hargoniX
refactor: bv_decide's type analysis to prepare for enum support (#6971)
4540a64 
This PR does some refactoring on bv_decide's type analysis in
preparation for enum support in #6946.
@hargoniX hargoniX force-pushed the hbv/bv_decide_enums branch from 571d882 to 2e2d566 Compare February 6, 2025 11:52
@hargoniX hargoniX force-pushed the hbv/bv_decide_enums branch from 2e2d566 to 011aa57 Compare February 10, 2025 09:09
@hargoniX hargoniX marked this pull request as ready for review February 10, 2025 09:13
@hargoniX hargoniX requested a review from kim-em as a code owner February 10, 2025 09:13
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 10, 2025 09:24 Inactive
@hargoniX hargoniX removed the request for review from kim-em February 10, 2025 09:39
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 10, 2025 09:42 Inactive
@hargoniX hargoniX enabled auto-merge February 10, 2025 09:46
@hargoniX hargoniX added this pull request to the merge queue Feb 10, 2025
Merged via the queue into master with commit 0d95bf6 Feb 10, 2025
15 checks passed
@hargoniX hargoniX deleted the hbv/bv_decide_enums branch February 10, 2025 10:34
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Feb 16, 2025
@hargoniX @tobiasgrosser
refactor: bv_decide's type analysis to prepare for enum support (lean…
ad7371d 
…prover#6971)

This PR does some refactoring on bv_decide's type analysis in
preparation for enum support in leanprover#6946.
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Feb 16, 2025
@hargoniX @tobiasgrosser
feat: basic support for handling enum inductives in bv_decide (leanpr…
db2b9e4 
…over#6946)

This PR implements basic support for handling of enum inductives in
`bv_decide`. It now supports equality on enum inductive variables (or
other uninterpreted atoms) and constants.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@hargoniX @luisacicolini
refactor: bv_decide's type analysis to prepare for enum support (lean…
6d03f7d 
…prover#6971)

This PR does some refactoring on bv_decide's type analysis in
preparation for enum support in leanprover#6946.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@hargoniX @luisacicolini
feat: basic support for handling enum inductives in bv_decide (leanpr…
b50a184 
…over#6946)

This PR implements basic support for handling of enum inductives in
`bv_decide`. It now supports equality on enum inductive variables (or
other uninterpreted atoms) and constants.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@hargoniX @luisacicolini
refactor: bv_decide's type analysis to prepare for enum support (lean…
3fd97ee 
…prover#6971)

This PR does some refactoring on bv_decide's type analysis in
preparation for enum support in leanprover#6946.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@hargoniX @luisacicolini
feat: basic support for handling enum inductives in bv_decide (leanpr…
f3ff133 
…over#6946)

This PR implements basic support for handling of enum inductives in
`bv_decide`. It now supports equality on enum inductive variables (or
other uninterpreted atoms) and constants.
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-language Language features, tactics, and metaprograms 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
@hargoniX @leanprover-community-bot