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.
assert
Def
b
== if
b
True else False fi
Thm*
b
:
.
b
Prop
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
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
list
1
Sections
MarkB
generic
Doc