fold and collapse sub-graph

ggrov / tinker

Graph based proof strategy language

http://ggrov.github.io/tinker/

6 stars 0 forks source link

fold and collapse sub-graph #4

Open lyhlbyl opened 10 years ago

lyhlbyl commented 10 years ago

when drawing a graph, user might want to

[x] 1. folder part of graph as a hierarchical node
[ ] 2. collapse a hierarchical node as sub-graph

plebras commented 10 years ago

n°1 done @lyhlbyl I am not sure what you meant in n°2 , is it the inverse action of n° 1

lyhlbyl commented 10 years ago

@plebras yes, it is an action of flatting a a sub-graph to the parent one.

ggrov commented 10 years ago

Note that 2 is non trivial as we have removed the requirement that children needs the same boundary as the parent. It should really only be handled in the core.