Commit 2025-11-20 13:23 bf9761c5

View on Github →

chore(Order/Defs/PartialOrder): fix naming of DecidableLE' (#31816) The rename DecidableGE -> DecidableLE' wasn't done everywhere, and this PR fixes that.

Estimated changes