WhoCites Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites list n?
list_nDef A List(n) == {x:(A List)| ||x|| = n   }
Thm* A:Type, n:A List(n Type
lengthDef ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
Thm* A:Type, l:A List. ||l||  
Thm* ||nil||  

Syntax:A List(n) has structure: list_n(An)

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

WhoCites Definitions StandardLib Sections NuprlLIB Doc