Idris2Doc : Data.Path

Data.Path

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 : Pathgii
(::) : gij -> Pathgjk -> Pathgik
foldPath : {0 gu : u -> u -> Type} -> {0 f : t -> u} -> (gtij -> gu (fj) (fk) -> gu (fi) (fk)) -> Pathgtij -> gu (fj) (fk) -> gu (fi) (fk)
Totality: total
foldlPath : {0 gu : u -> u -> Type} -> {0 f : t -> u} -> (gu (fi) (fj) -> gtjk -> gu (fi) (fk)) -> gu (fi) (fj) -> Pathgtjk -> gu (fi) (fk)
Totality: total
joinPath : Pathgij -> Pathgjk -> Pathgik
Totality: total
lengthPath : Pathgij -> Nat
Totality: total
mapPath : {0 f : t -> u} -> (gtij -> gu (fi) (fj)) -> Pathgtij -> Pathgu (fi) (fj)
Totality: total
snocPath : Pathgij -> gjk -> Pathgik
Totality: total