size
(size List)
Type
i.filter(j.f(i,j);upto(0;n)))
m:AdjMatrix. adjm_to_adjl(m) AdjListsizesize
Type| Some definitions of interest. | |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| adjm_to_adjl | Def adjm_to_adjl(m) == Case(m) Case mk_adjmatrix(n,f) = > mk_adjlist(n, i.filter(j.f(i,j);upto(0;n))) |
| Thm* m:AdjMatrix. adjm_to_adjl(m) AdjList | |
| adjmatrix | Def AdjMatrix == size:sizesize |
| Thm* AdjMatrix Type |
About:
 |  |  |  |  |  |
 |  |  |  |  |