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.
filter
Def
filter(
P
;
l
) == reduce(
a
,
v
. if
P
(
a
)
[
a
/
v
] else
v
fi;nil;
l
)
Thm*
T
:Type,
P
:(
T
),
l
:
T
List. filter(
P
;
l
)
T
List
iseg
Def
l1
l2
==
l
:
T
List.
l2
= (
l1
@
l
)
Thm*
T
:Type,
l1
,
l2
:
T
List.
l1
l2
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
list
1
Sections
MarkB
generic
Doc