ControlFlow.Edge

Definitions

data Edge : Type -> Type

  An edge between vertices
  @ a the type of vertex identifiers

Totality: total
Visibility: public export
Constructor: 

(~>) : a -> a -> Edge a

  `v ~> w` - an edge from `v` to `w`

(<~) : a -> a -> Edge a

Visibility: public export
Fixity Declarations:
infix operator, level 6
infixl operator, level 0

Dest : Edge a -> a

Visibility: public export

Origin : Edge a -> a

Visibility: public export

(~~>) : List a -> a -> List (Edge a)

  A *collection* of `vs` by `v`

Visibility: public export
Fixity Declaration: infix operator, level 8

(~>>) : a -> List a -> List (Edge a)

  A *distribution* of `v` to `vs`

Visibility: public export
Fixity Declaration: infix operator, level 8

(<~~) : a -> List a -> List (Edge a)

  Flipped `(~~>)`

Visibility: public export
Fixity Declaration: infix operator, level 8

(<<~) : List a -> a -> List (Edge a)

  Flipped `(~>>)`

Visibility: public export
Fixity Declaration: infix operator, level 8

collect_concat : (v : a) -> (vs : List a) -> (ws : List a) -> (vs ++ ws) ~~> v = (vs ~~> v) ++ (ws ~~> v)

     A collection    of a   concatenation of two   lists by `v`
  is a concatenation of the collections   of these lists by `v`

Visibility: export

distribute_concat : (v : a) -> (vs : List a) -> (ws : List a) -> v ~>> (vs ++ ws) = (v ~>> vs) ++ (v ~>> ws)

     A distribution  of `v` to a   concatenation        of two   lists
  is a concatenation        of the distributions of `v` to these lists

Visibility: export

collect_append : (v : a) -> (vs : List a) -> (w : a) -> (vs ++ [w]) ~~> v = (vs ~~> v) ++ [(w ~> v)]

  A special case of `collect_concat` where `ws` is a singleton

Visibility: export

distribute_append : (v : a) -> (vs : List a) -> (w : a) -> v ~>> (vs ++ [w]) = (v ~>> vs) ++ [(v ~> w)]

  A special case of `distribute_concat` where `ws` is a singleton

Visibility: export