WhoCites Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites zip?
zipDef zip(as;bs)
Def == Case of as
Def == Canil  nil
Def == Caa.as'  Case of bs; nil  nil ; b.bs'  [<a,b> / zip(as';bs')]
Def (recursive)
Thm* T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs (T1T2) List

Syntax:zip(as;bs) has structure: zip(asbs)

About:
pairproductlistconsnillist_ind
recursive_def_noticeuniversememberall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions mb list 1 Sections MarkB generic Doc