Data.Graph.Indexed.Ring.Util

Definitions

0 EdgeSet : Nat -> Type

  A set of unlabeled edges of order `k`

Totality: total
Visibility: public export

addEdge : EdgeSet k -> Fin k -> Fin k -> EdgeSet k

  Adds an unlabeled edge to an edge set.
  
  The edge set is returned unmodified, if the two nodes are
  identical.

Totality: total
Visibility: export

addNatEdge : EdgeSet k -> Nat -> Nat -> EdgeSet k

  Adds an unlabeled edge to an edge set.
  
  The edge set is returned unmodified, if the two natural numbers
  are not valid distinct nodes of order `k`.

Totality: total
Visibility: export

toEdgeSet : List (Nat, Nat) -> EdgeSet k

  Converts a list of pairs of natural number to an edge set of
  order `k`. Invalid pairs of nodes are silently dropped.

Totality: total
Visibility: export

inThreeMemberedRing : IGraph k e n -> Fin k -> Bool

  True, if the given node is a member of a three-membered cycle.
  
  For sparse graphs, this check can be performed in linear time without
  performing a proper ring detection, just be checking if two of the
  neighbours of the given node are adjacent.

Totality: total
Visibility: export