Data.Path

Definitions

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
Visibility: public export
Constructors:

Nil : Path g i i

(::) : g i j -> Path g j k -> Path g i k

joinPath : Path g i j -> Path g j k -> Path g i k

Totality: total
Visibility: export

snocPath : Path g i j -> g j k -> Path g i k

Totality: total
Visibility: export

lengthPath : Path g i j -> Nat

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

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
Visibility: export