ord

Ordering

data Ordering

The result of a three-way comparison: less than, equal, or greater than.

Ordering.flip

def flip (o : Ordering) : Ordering

The comparison the other way round: LT and GT swap.

Ordering.isLT

def isLT (o : Ordering) : Bool

Whether it is LT.

Ordering.isEQ

def isEQ (o : Ordering) : Bool

Whether it is EQ.

Ordering.isGT

def isGT (o : Ordering) : Bool

Whether it is GT.

Ordering.isLE

def isLE (o : Ordering) : Bool

Whether it is LT or EQ.

Ordering.isGE

def isGE (o : Ordering) : Bool

Whether it is GT or EQ.

Ordering.beq

def beq (a : Ordering) (b : Ordering) : Bool

Whether two results are the same.

Ordering.then

def r#then (a : Ordering) (b : Ordering) : Ordering

A comparison by two keys: a unless it is EQ, then b (compare x y |>.then (compare u v)).

minBy

def minBy {A : Type} (cmp : A -> A -> Ordering) (a : A) (b : A) : A

The smaller of two values under a comparison (the first when they compare equal).

maxBy

def maxBy {A : Type} (cmp : A -> A -> Ordering) (a : A) (b : A) : A

The larger of two values under a comparison (the first when they compare equal).

Nat.threeWayStructurally

def Nat.threeWayStructurally (m : Nat) (n : Nat) : Ordering

Comparison of naturals by structural recursion (for proofs by induction; programs use Nat.threeWay).

Nat.threeWay

def Nat.threeWay (m : Nat) (n : Nat) : Ordering

Comparison of naturals for programs: the accelerated Nat.blt and Nat.beq, constant steps on literals.

Nat.threeWayEqStructurally

def Nat.threeWayEqStructurally (m : Nat) (n : Nat) : Nat.threeWay m n = Nat.threeWayStructurally m n

The two comparisons of naturals agree.

Bool.threeWay

def Bool.threeWay (a : Bool) (b : Bool) : Ordering

Comparison of Booleans, false before true.

String.threeWayChars

def String.threeWayChars (xs : List Char) (ys : List Char) : Ordering

Lexicographic comparison of characters by code point; a proper prefix comes first.

String.threeWay

def String.threeWay (a : String) (b : String) : Ordering

Lexicographic comparison of strings by code point (which is the order of their UTF-8 bytes).

Ord

class Ord (A : Type)

A total order: compare a b is where a stands relative to b.

ordNat

instance ordNat : Ord Nat

Naturals by value.

ordBool

instance ordBool : Ord Bool

Booleans, false first.

ordChar

instance ordChar : Ord Char

Characters by code point.

ordString

instance ordString : Ord String

Strings lexicographically.

List.mergeBy

def mergeBy {A : Type} (cmp : A -> A -> Ordering) (fuel : Nat) (xs : List A) (ys : List A) : List A

Two lists sorted by cmp merged; on a tie the element of xs comes first (the merge is stable). fuel only bounds the recursion for the termination checker.

List.sortWithin

def sortWithin {A : Type} (cmp : A -> A -> Ordering) (fuel : Nat) (xs : List A) : List A

Merge sort within fuel rounds: halves sorted and merged.

List.sortBy

def sortBy {A : Type} (cmp : A -> A -> Ordering) (xs : List A) : List A

A list sorted by a comparison, stably (equal elements keep their order).

List.sort

def sort {A : Type} {{o : Ord A}} (xs : List A) : List A

A list sorted by its order, ascending.

List.sortOn

def sortOn {A : Type} {B : Type} {{o : Ord B}} (key : A -> B) (xs : List A) : List A

A list sorted by a key of each element, ascending and stably.

List.dropRepeats

def dropRepeats {A : Type} {{o : Ord A}} (xs : List A) : List A

A sorted list with each run of equal elements kept once.

List.distinct

def distinct {A : Type} {{o : Ord A}} (xs : List A) : List A

The distinct elements of a list, ascending.