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.
iff
Def
P
Q
== (
P
Q
) & (
P
Q
)
Thm*
A
,
B
:Prop. (
A
B
)
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
mb
list
1
Sections
MarkB
generic
Doc