Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
ge
Def
i
j
==
j
i
Thm*
i
,
j
:
. (
i
j
)
Prop
length
Def
||
as
|| == Case of
as
; nil
0 ;
a
.
as'
||
as'
||+1 (recursive)
Thm*
A
:Type,
l
:
A
List. ||
l
||
Thm*
||nil||
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
list
1
Sections
StandardLIB
Doc
j == j
i
i,j:
. (ij) 
Prop
0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| j == jii,j:. (ij) Prop 0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| 
