Idris2Doc : Data.Graph.Indexed.Query.Util

Data.Graph.Indexed.Query.Util

(source)
Utilities for graph traversals.

Definitions

fromLeft : Either a Void -> a
  Extract a value from a `Left` because we know the `Right` is
uninhabited.

Totality: total
Visibility: public export
fleft2 : (a -> b -> c) -> a -> b -> Either c Void
  Convert a binary function to one returning an `Left`

Totality: total
Visibility: public export
fleft3 : (a -> b -> c -> d) -> a -> b -> c -> Either d Void
  Convert a ternary function to one returning an `Left`

Totality: total
Visibility: public export
0 MVis : Type -> Nat -> Type -> Type
  Internal alias for stateful functions when visiting large graphs

Totality: total
Visibility: public export
fromLeftMVis : R1 s (Either a Void) -@ R1 s a
Totality: total
Visibility: export