WhoCites Definitions mb automata 3 Sections GenAutomata Doc

Who Cites zip?
zipDef zip(as;bs) == Case of as; nil nil ; a.as' Case of bs; nil nil ; b.bs' [ < a,b > / zip(as';bs')] (recursive)
Thm* T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs) (T1T2) List

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

About:
pairproductlistconsnillist_ind
recursive_def_noticeuniversememberall!abstraction

WhoCites Definitions mb automata 3 Sections GenAutomata Doc