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_n
Def
A
List(
n
) == {
x
:(
A
List)| ||
x
|| =
n
}
Thm*
A
:Type,
n
:
.
A
List(
n
)
Type
length
Def
||
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(
A
;
n
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc