is mentioned by

Def adjm-edge-accum(M;s',x'.f(s';x');s;x) == primrec(M.size;s;y,s'. if M.adj(x,y) f(s';y) else s' fi)	[adjm-edge-accum]
Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e >	[adjm-graph]

Try larger context: Graphs