Skip to content

feat: add a Decidable instance for bif (cond) - #15018

Merged
TwoFX merged 1 commit into
leanprover:masterfrom
marcusrossel:master
Sep 4, 2026
Merged

feat: add a Decidable instance for bif (cond)#15018
TwoFX merged 1 commit into
leanprover:masterfrom
marcusrossel:master

Conversation

@marcusrossel

Copy link
Copy Markdown
Contributor

This PR adds a missing Decidable instance for bif (cond) expressions, analogous to the existing instance for if (ite) expressions.

Discussed in https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Decidable.20bif/near/621670745.

@github-actions github-actions Bot added awaiting-review Waiting for someone to review the PR changelog-added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Sep 4, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 67526ae54d733251644d5cebb9fa5a77318fecc4 --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-04 11:46:19)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 67526ae54d733251644d5cebb9fa5a77318fecc4 --onto 58774429865502f05c63239266aac30ef1e91ef7. You can force reference manual CI using the force-manual-ci label. (2026-09-04 11:46:21)

@TwoFX TwoFX added changelog-library Library and removed changelog-added awaiting-review Waiting for someone to review the PR changelog-library Library labels Sep 4, 2026

@TwoFX TwoFX left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX
TwoFX added this pull request to the merge queue Sep 4, 2026
Merged via the queue into leanprover:master with commit 3dfca7a Sep 4, 2026
43 of 46 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants