Safe Haskell | None |
---|---|

Language | Haskell2010 |

Insert an edge into a set. `X -> Y e`

with `e == Edge`

extends `Y`

with the edge partially overlapping `Y`

.

The semantic meaning of the overlap depends on what the `k`

type in ```
BS1
k i
```

is. For `First`

, the edge will go from `First`

in `X`

to `First`

in
the smaller `Y`

.

TODO `X -> e X`

vs `X -> X e`

.

Sidenote: can we actually have `X -> Y Z`

with `Set1`

structures?
I don't think so, at least not easily, since the boundary between `Y Z`

is unclear.

# Documentation

class EdgeFromTo k where Source #

TODO move to definition of `Edge`

EdgeFromTo First Source # | In case our sets have a |

EdgeFromTo Last Source # | And if the set has a |

# Orphan instances

TermStaticVar Edge (BS1 k I) Source # | |

(TstCtx m ts s x0 i0 is (BS1 k I), EdgeFromTo k) => TermStream m (TermSymbol ts Edge) s ((:.) is (BS1 k I)) Source # | We need to separate out the two cases of having TODO separate out these cases into an Edge-Choice class ... |

TmkCtx1 m ls Edge (BS1 k t) => MkStream m ((:!:) ls Edge) (BS1 k t) Source # | |