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.
length
Def
||
as
|| == Case of
as
; nil
0 ;
a
.
as'
||
as'
||+1 (recursive)
Thm*
A
:Type,
l
:
A
List. ||
l
||
Thm*
||nil||
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
list
1
Sections
MarkB
generic
Doc
0 ; a.as' ||as'||+1 (recursive)
A:Type, l:A List. ||l|| 
== {i:| 0
i } Type 0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| == {i:| 0i } Type
