Sorted.idr

module Sorted

data LessThanOrEq : (x,y : type)
              -> Type
  where
    IsLessThan : Ord type => {x,y : type} -> (prf : compare x y = LT) -> LessThanOrEq x y
    IsEqual    : Ord type => {x,y : type} -> (prf : compare x y = EQ) -> LessThanOrEq x y

data IsSorted : (list : List type)
             -> Type
  where
    Empty  : IsSorted Nil
    Single : IsSorted [x]
    Pair   : (prf : LessThanOrEq x y)
          -> IsSorted (y::rest)
          -> IsSorted (x::y::rest)

prf : Ord a => (xs : List a) -> {auto prf : IsSorted xs} -> IsSorted xs
prf xs {prf} = prf