mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore: Move Nat.instLinearOrder to Init.Order.Defs

Open Ruben-VandeVelde opened this issue 8 months ago • 10 comments

It turns out that pushing the dependency out is quite annoying, so as an alternative, we propose considering Preorder, PartialOrder and LinearOrder to be foundational type classes that all of Mathlib can depend on.

Open in Gitpod

Ruben-VandeVelde avatar Jun 24 '24 09:06 Ruben-VandeVelde