Agda-2.2.8: A dependently typed functional programming language and proof assistant

Agda.Utils.Graph

newtype Graph n e Source

Constructors

Fields

edges :: Ord n => Graph n e -> [(n, n, e)]Source

nodes :: Ord n => Graph n e -> Set nSource

fromList :: (SemiRing e, Ord n) => [(n, n, e)] -> Graph n eSource

empty :: Graph n eSource

singleton :: n -> n -> e -> Graph n eSource

insert :: (SemiRing e, Ord n) => n -> n -> e -> Graph n e -> Graph n eSource

union :: (SemiRing e, Ord n) => Graph n e -> Graph n e -> Graph n eSource

unions :: (SemiRing e, Ord n) => [Graph n e] -> Graph n eSource

lookup :: Ord n => n -> n -> Graph n e -> Maybe eSource

neighbours :: Ord n => n -> Graph n e -> [(n, e)]Source

growGraph :: (SemiRing e, Ord n) => Graph n e -> Graph n eSource

transitiveClosure :: (SemiRing e, Ord n) => Graph n e -> Graph n eSource

findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n e -> Maybe eSource

allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n e -> [e]Source