Data.List.Quantifiers.Extra

Reexports

Definitions

0 HSum : List Type -> Type

  Just like `HList` is an alias for `All id`, this is an
  alias for `Any id`.

Totality: total
Visibility: public export

0 Has : a -> List a -> Type

  Proof that a value is present in a list. This is
  just an alias for `Data.List.Elem` with a name that's
  sometimes more fitting.

Totality: total
Visibility: public export

negate : Neg ty => ty -> ty

  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

0 (-) : (ts : List a) -> (v : a) -> Has v ts => List a

  Removes an element from a list. This is used to
  calculate the list of effects after a single effect
  was properly handled.

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10

inject : Has t ts => f t -> Any f ts

  Inject a value into a `Any f ts`.

Totality: total
Visibility: public export

widen : All (\{arg:0} => Has {arg:0} ts) ss => Any f ss -> Any f ts

  Injects a heterogeneous sum into a larger one.

Totality: total
Visibility: public export

project : (0 t : k) -> Has t ts => Any f ts -> Maybe (f t)

  Tries to extract a value from a `Any f ts`.

Totality: total
Visibility: public export

project' : Has t ts => Any f ts -> Maybe (f t)

  Tries to extract a value from a `Any f ts`.

Totality: total
Visibility: public export

project1 : Any f [t] -> f t

  Extracts the only possible value from a unary sum.

Totality: total
Visibility: public export

decomp : {auto prf : Has t ts} -> Any f ts -> Either (Any f (ts - t)) (f t)

  Extract one of the values from an `Any f ts`.

Totality: total
Visibility: public export

hmap : (f v -> g v) -> Any f ks -> Any g ks

Totality: total
Visibility: public export

hzipWith : (f v -> g v -> h v) -> All f ks -> Any g ks -> Any h ks

Totality: total
Visibility: public export

collapse : (f v -> x) -> Any f ks -> x

Totality: total
Visibility: public export

collapse' : Any (const x) ks -> x

Totality: total
Visibility: public export

hsequence : Applicative f => Any (f . g) ks -> f (Any g ks)

Totality: total
Visibility: public export

hmap : (f v -> g v) -> All f ks -> All g ks

Totality: total
Visibility: public export

hmapW : ((v : k) -> f v -> g v) -> All f ks -> All g ks

Totality: total
Visibility: public export

hzipWith : (f v -> g v -> h v) -> All f ks -> All g ks -> All h ks

Totality: total
Visibility: public export

hzipWithW : ((v : k) -> f v -> g v -> h v) -> All f ks -> All g ks -> All h ks

Totality: total
Visibility: public export

happly : All (\x => f x -> g x) ks -> Any f ks -> Any g ks

Totality: total
Visibility: public export

happly' : All (\x => f x -> t) ks -> Any f ks -> t

Totality: total
Visibility: public export

hfill : ((v : k) -> f v) -> All f ks

Totality: total
Visibility: public export

hconst : t -> All (const t) ks

Totality: total
Visibility: public export

hpure : All (const ()) ks => f v -> All f ks

Totality: total
Visibility: public export

hfoldl : (acc -> f v -> acc) -> acc -> All f ks -> acc

Totality: total
Visibility: public export

hfoldMap : Monoid m => (f v -> m) -> All f ks -> m

Totality: total
Visibility: public export

hsequence : Applicative f => All (f . g) ks -> f (All g ks)

Totality: total
Visibility: public export