Minimum and maximum of lists #
Main definitions #
The main definitions are argmax
, argmin
, minimum
and maximum
for lists.
argmax f l
returns some a
, where a
of l
that maximises f a
. If there are a b
such that
f a = f b
, it returns whichever of a
or b
comes first in the list.
argmax f [] = none
minimum l
returns a WithTop α
, the smallest element of l
for nonempty lists, and ⊤
for
[]
Auxiliary definition for argmax
and argmin
.
Equations
- List.argAux r a b = Option.casesOn a (some b) fun c => if r b c then some b else some c
Instances For
argmax f l
returns some a
, where f a
is maximal among the elements of l
, in the sense
that there is no b ∈ l
with f a < f b
. If a
, b
are such that f a = f b
, it returns
whichever of a
or b
comes first in the list. argmax f [] = none
.
Equations
- List.argmax f l = List.foldl (List.argAux fun b c => f c < f b) none l
Instances For
argmin f l
returns some a
, where f a
is minimal among the elements of l
, in the sense
that there is no b ∈ l
with f b < f a
. If a
, b
are such that f a = f b
, it returns
whichever of a
or b
comes first in the list. argmin f [] = none
.
Equations
- List.argmin f l = List.foldl (List.argAux fun b c => f b < f c) none l
Instances For
maximum l
returns a WithBot α
, the largest element of l
for nonempty lists, and ⊥
for
[]
Equations
- List.maximum l = List.argmax id l
Instances For
minimum l
returns a WithTop α
, the smallest element of l
for nonempty lists, and ⊤
for
[]
Equations
- List.minimum l = List.argmin id l
Instances For
The maximum value in a non-empty List
.
Equations
- List.maximum_of_length_pos h = WithBot.unbot (List.maximum l) (_ : List.maximum l ≠ ⊥)
Instances For
The minimum value in a non-empty List
.