Commit 2026-06-17 15:42 9d11f4f0

feat(Tactic/Positivity): make positivity work for types that are not partial orders (#35394) Make positivity work for types that are not partial orders Most PositivityExt haven't been updated for non partial order cases yet. They will be updated in the later PR. Strictness now depends on Option Q(PartialOrder $α) instead of Q(PartialOrder $α), and the constructors Strictness.positive/Strictness.nonnegative now have their Q(PartialOrder $α) typeclass arguments.