Documentation

Init.Data.Nat.Order

← Mathematical handbook
source
instance Nat.instIsLinearOrder :
Std.IsLinearOrder Nat
source
instance Nat.instLawfulOrderLT :
Std.LawfulOrderLT Nat
source
instance Nat.instLawfulOrderMin :
Std.LawfulOrderMin Nat
source
instance Nat.instLawfulOrderMax :
Std.LawfulOrderMax Nat