PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter
type
T
:Type,
P
:(
T
),
l
:
T
List. filter(
P
;
l
)
{
x
:
T
|
P
(
x
) } List
By:
InductionOnList THEN Reduce 0 THEN Try (Complete Auto) THEN SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, P:(T
), l:T List. filter(P;l) 
{x:T| P(x) } List T:Type, P:(T), l:T List. filter(P;l) {x:T| P(x) } List
