Documentation
Init
.
Data
.
Ord
Search
Google site search
Init
.
Data
.
Ord
source
Imports
Init.Data.Int
Init.Data.String
Imported by
Ordering
instInhabitedOrdering
instBEqOrdering
Ord
compareOfLessAndEq
instOrdNat
instOrdInt
instOrdBool
instOrdString
instOrdFin
instOrdUInt8
instOrdUInt16
instOrdUInt32
instOrdUInt64
instOrdUSize
instOrdChar
lexOrd
ltOfOrd
instDecidableRelLtLtOfOrd
Ordering
.
isLE
leOfOrd
instDecidableRelLeLeOfOrd
source
inductive
Ordering
:
Type
lt:
Ordering
eq:
Ordering
gt:
Ordering
Instances For
source
instance
instInhabitedOrdering
:
Inhabited
Ordering
source
instance
instBEqOrdering
:
BEq
Ordering
source
class
Ord
(α :
Type
u)
:
Type
u
compare :
α
→
α
→
Ordering
Instances
source
@[inline]
def
compareOfLessAndEq
{α :
Type
u_1}
(x :
α
)
(y :
α
)
[
LT
α
]
[
Decidable
(
x
<
y
)
]
[
DecidableEq
α
]
:
Ordering
Instances For
source
instance
instOrdNat
:
Ord
Nat
source
instance
instOrdInt
:
Ord
Int
source
instance
instOrdBool
:
Ord
Bool
source
instance
instOrdString
:
Ord
String
source
instance
instOrdFin
(n :
Nat
)
:
Ord
(
Fin
n
)
source
instance
instOrdUInt8
:
Ord
UInt8
source
instance
instOrdUInt16
:
Ord
UInt16
source
instance
instOrdUInt32
:
Ord
UInt32
source
instance
instOrdUInt64
:
Ord
UInt64
source
instance
instOrdUSize
:
Ord
USize
source
instance
instOrdChar
:
Ord
Char
source
def
lexOrd
{α :
Type
u_1}
{β :
Type
u_2}
[
Ord
α
]
[
Ord
β
]
:
Ord
(
α
×
β
)
The lexicographic order on pairs.
Instances For
source
def
ltOfOrd
{α :
Type
u_1}
[
Ord
α
]
:
LT
α
Instances For
source
instance
instDecidableRelLtLtOfOrd
{α :
Type
u_1}
[
Ord
α
]
:
DecidableRel
LT.lt
source
def
Ordering
.
isLE
:
Ordering
→
Bool
Instances For
source
def
leOfOrd
{α :
Type
u_1}
[
Ord
α
]
:
LE
α
Instances For
source
instance
instDecidableRelLeLeOfOrd
{α :
Type
u_1}
[
Ord
α
]
:
DecidableRel
LE.le