Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
isegDef l1  l2 == l:T List. l2 = (l1 @ l)
Thm* T:Type, l1,l2:T List. l1  l2  Prop
appendDef as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
Thm* T:Type, as,bs:T List. (as @ bs T List
firstnDef firstn(n;as)
Def == Case of as
Def == Canil  nil
Def == Caa.as'  if 0<n [a / firstn(n-1;as')] else nil fi
Def (recursive)
Thm* A:Type, as:A List, n:. firstn(n;as A List
iffDef P  Q == (P  Q) & (P  Q)
Thm* A,B:Prop. (A  B Prop
int_segDef {i..j} == {k:i  k < j }
Thm* m,n:. {m..n Type
lengthDef ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
Thm* A:Type, l:A List. ||l||  
Thm* ||nil||  

About:
listconsnillist_ind
ifthenelseintnatural_numberaddsubtractset
recursive_def_noticeuniverseequalmemberpropimpliesandall
exists!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb list 1 Sections MarkB generic Doc