code.lol
/ bytes
Init
.
Data
.
Nat
.
Order
Search
return to top
source
Imports
Init.NotationExtra
Init.Data.Nat.Basic
Init.Data.Nat.MinMax
Init.Data.Order.Classes
Init.Data.Order.Factories
Imported by
Nat
.
instIsLinearOrder
Nat
.
instLawfulOrderLT
Nat
.
instLawfulOrderMin
Nat
.
instLawfulOrderMax
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