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
[]
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
.
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
.
Instances For
maximum l
returns a WithBot α
, the largest element of l
for nonempty lists, and ⊥
for
[]
Instances For
minimum l
returns a WithTop α
, the smallest element of l
for nonempty lists, and ⊤
for
[]
Instances For
The maximum value in a non-empty List
.
Instances For
The minimum value in a non-empty List
.