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