Commit 2024-05-08 18:28 59b7bc48
View on Github →refactor(Opposite): Opposite.mk -> Opposite.op (#12636)
It was observed on Zulip that we should really have op as the custom name for the Opposite constructor as long as it remains a structure.