Idris2Doc : Data.Profunctor.Sieve

Data.Profunctor.Sieve

(source)

Definitions

interface Sieve : (Type -> Type -> Type) -> (Type -> Type) -> Type
  A profunctor `p` is a sieve on `f` if it is a subprofunctor of `Star f`.

Parameters: p, f
Constraints: Profunctor p, Functor f
Methods:
sieve : p a b -> a -> f b

Implementations:
Sieve Morphism Identity
Functor f => Sieve (Kleislimorphism f) f
Functor f => Sieve (Star f) f
Sieve (Forget r) (Const r)
sieve : Sieve p f => p a b -> a -> f b
Totality: total
Visibility: public export
interface Cosieve : (Type -> Type -> Type) -> (Type -> Type) -> Type
  A profunctor `p` is a cosieve on `f` if it is a subprofunctor of `Costar f`.

Parameters: p, f
Constraints: Profunctor p, Functor f
Methods:
cosieve : p a b -> f a -> b

Implementations:
Cosieve Morphism Identity
Functor f => Cosieve (Costar f) f
Cosieve (Coforget r) (Const r)
cosieve : Cosieve p f => p a b -> f a -> b
Totality: total
Visibility: public export