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)