Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* T:(Id), to,from:(|T|(IdLnk List)). Thm* bi-tree(T;to;from)  (n:. p:Edge(T) List. lpath(p)  ||p||n)	[bi-tree-diameter]
Thm* R:(Id), in,out:(|R|IdLnk). Thm* ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L)))	[ring-list]

In prior sections: list 1 mb basic mb nat mb list 1 mb list 2 mb event system 1 mb event system 2 mb event system 3

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html