Skip to content

feat: new deriving handlers for BEq, Ord, ReflBEq and ReflOrd - #14929

Draft
Rob23oba wants to merge 7 commits into
leanprover:masterfrom
Rob23oba:deriving-beq-ord-better
Draft

feat: new deriving handlers for BEq, Ord, ReflBEq and ReflOrd#14929
Rob23oba wants to merge 7 commits into
leanprover:masterfrom
Rob23oba:deriving-beq-ord-better

Conversation

@Rob23oba

Copy link
Copy Markdown
Contributor

This PR adds new deriving handlers for BEq, Ord, ReflBEq and ReflOrd as well as a new framework for deriving handlers.

TODO: split

@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 Aug 25, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 25, 2026

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 47680c2e62831da4daa01abe567b3e4fc509fbae --onto 4620e4d946957ae7c582764c79eb93cc779f77e2. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 18:55:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47680c2e62831da4daa01abe567b3e4fc509fbae --onto b9c9eb9a3acefaa242c1da2a31e3723e94fde3a5. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-26 16:47:03)

@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 47680c2e62831da4daa01abe567b3e4fc509fbae --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-25 18:55:09)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

2 participants