
  0 | ||| An attempt at a class of functors defined on a subclass of Type.
  1 | module Data.Functor.Restricted
  2 | 
  3 | import Data.SortedMap
  4 | import Data.SortedSet
  5 | 
  6 | 
  7 | public export
  8 | interface RFunctor (0 r : Type -> Type) (0 f : Type -> Type) | f where
  9 |   rmap : (r x, r y) => (x -> y) -> f x -> f y
 10 | 
 11 | RFunctor Ord SortedSet where
 12 |   rmap f = fromList . map f . Prelude.toList
 13 |