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.
assertDef b == if b True else False fi
Thm* b:b  Prop
lastDef last(L) == L[(||L||-1)]
Thm* T:Type, L:T List. null(L last(L T
leDef AB == B<A
Thm* i,j:. (ij Prop
lengthDef ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
Thm* A:Type, l:A List. ||l||  
Thm* ||nil||  
notDef A == A  False
Thm* A:Prop. (A Prop
nullDef null(as) == Case of as; nil  true ; a.as'  false
Thm* T:Type, as:T List. null(as 
Thm* null(nil)  

About:
listnillist_indboolbfalse
btrueifthenelseassertintnatural_numberaddsubtractless_than
recursive_def_noticeuniversememberpropimpliesfalsetrue
all!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb list 1 Sections MarkB generic Doc