graph 1 3 Sections Graphs Doc

Def {i..j} == {k:| i k < j }

is mentioned by

Thm* t:AdjList. t.out t.size(t.size List)[adjl_out_wf]
Thm* t:AdjMatrix. t.adj t.sizet.size[adjm_adj_wf]
Def adjl-graph(G) == < vertices = G.size, edges = x:G.size||G.out(x)||, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > > [adjl-graph]
Def AdjList == size:size(size List)[adjlist]
Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e > [adjm-graph]
Def AdjMatrix == size:sizesize[adjmatrix]

In prior sections: int 1 bool 1 int 2 list 1 mb basic mb nat mb list 1 num thy 1 mb list 2 graph 1 1 graph 1 2 prog 1

Try larger context: Graphs

graph 1 3 Sections Graphs Doc