peano-inf-0.6.1: Number/Peano/Inf/Functions.hs
module Number.Peano.Inf.Functions
( minimum
, maximum
, length
) where
import Number.Peano.Inf
import qualified Prelude as P
import Prelude hiding (minimum, maximum, length)
{- |
Minimum of the list elements.
Works also for empty lists.
-}
minimum :: [Nat] -> Nat
minimum = foldr min infinity
{- |
Maximum of the list elements.
Works also for empty lists.
-}
maximum :: [Nat] -> Nat
maximum = foldr max 0
{- |
Lazyness properties of @Nat@ makes it ideal for lazy list length computation.
Examples:
> length [1..] > 100
> length undefined >= 0
> length (undefined: undefined) >= 1
-}
length :: [a] -> Nat
length [] = 0
length (_:t) = succ (length t)