Abstract Refinements

Ordered Lists

Previously we saw how to refine the list data definition to get ordered lists:

{-@ data OList a =
     OEmp
   | (:<:) { oHd :: a
           , oTl :: OList {v:a | oHd <= v}} @-}