Documentation
Init
.
Data
.
Char
.
Order
Search
return to top
source
Imports
Init.PropLemmas
Init.Data.Char.Basic
Init.Data.Char.Lemmas
Init.Data.Order.Classes
Init.Data.Order.Factories
Imported by
Char
.
instIsLinearOrder
Char
.
instLawfulOrderLT
← Mathematical handbook
source
instance
Char
.
instIsLinearOrder
:
Std.IsLinearOrder
Char
source
instance
Char
.
instLawfulOrderLT
:
Std.LawfulOrderLT
Char