Commit 2025-10-28 10:18 671b456b
View on Github →chore(without_cdot): remove all uses of without_cdot (#30735)
This PR removes all 2 uses of without_cdot. It is not needed anymore, because Lean automatically avoids accidental cdot capture. without_cdot may be deprecated in a future PR.