(8steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
listify
wf
1
1
2
1.
T
: Type
2.
k
:
3.
k1
:
.
k1
<
k
(
m
,
n
:
.
n
-
m
k1
(
f
:({
m
..
n
}
T
).
f
{
m
..
n
}
T
List))
4.
m
:
5.
n
:
6.
n
-
m
k
7.
f
: {
m
..
n
}
T
8.
m
<
n
f
(
m
).
f
{(
m
+1)..
n
}
T
List
By:
Analyze
Generated subgoals:
1
f
(
m
)
T
Auto
2
f
{(
m
+1)..
n
}
T
List
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc