Idris2Doc : Data.Path

Data.Path

data Path : (t -> t -> Type) -> t -> t -> Type
  Paths in a typed graph as a sequence of edges with source and target nodes matching up domino-style.
  AKA reflexive-transitive closure.

  Totality: total
  Constructors:
  
Nil : Path g i i
  
(::) : g i j -> Path g j k -> Path g i k
foldPath : {0 gu : u -> u -> Type} -> {0 f : t -> u} -> (gt i j -> gu (f j) (f k) -> gu (f i) (f k)) -> Path gt i j -> gu (f j) (f k) -> gu (f i) (f k)
  Totality: total
foldlPath : {0 gu : u -> u -> Type} -> {0 f : t -> u} -> (gu (f i) (f j) -> gt j k -> gu (f i) (f k)) -> gu (f i) (f j) -> Path gt j k -> gu (f i) (f k)
  Totality: total
joinPath : Path g i j -> Path g j k -> Path g i k
  Totality: total
lengthPath : Path g i j -> Nat
  Totality: total
mapPath : {0 f : t -> u} -> (gt i j -> gu (f i) (f j)) -> Path gt i j -> Path gu (f i) (f j)
  Totality: total
snocPath : Path g i j -> g j k -> Path g i k
  Totality: total