G.size, edges = x:G.size
||G.out(x)||, incidence = 
e. < 1of(e),(G.out(1of(e)))[2of(e)] > > size
(size List)
Typee:Type(evv)Top Type{i'}| Some definitions of interest. | |
| adjl-graph | Def adjl-graph(G) == < vertices = G.size, edges = x:G.size||G.out(x)||, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > > |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |