lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

chore: make `Subrelation` reducible

Open fgdorais opened this issue 3 months ago • 4 comments

This PR makes Subrelation reducible.

Closes #10471

fgdorais avatar Sep 19 '25 20:09 fgdorais

WIP

fgdorais avatar Sep 19 '25 20:09 fgdorais

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 38b4062edb5f14185df19d702953756f48ceaba0 --onto 4379002d0582ae96d7fc6ccf5921ff4e9aa7239e. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-19 21:21:53)

leanprover-community-bot avatar Sep 19 '25 21:09 leanprover-community-bot

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 38b4062edb5f14185df19d702953756f48ceaba0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-19 21:21:54)

leanprover-bot avatar Sep 19 '25 21:09 leanprover-bot

awaiting-review

fgdorais avatar Sep 19 '25 23:09 fgdorais