(37steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list
iso
2
2
1
1
1
2
1.
'a
: S
2.
x
: (
'a
)
3.
f
:
'a
4.
n
:
5.
x
= <
m
:
. if
m
<
n
then
f
(
m
) else @
x
:
'a
. true
fi ,
n
>
<
m
:
. if
m
<
n
then
f
(
m
) else @
x
:
'a
. true
fi ,
n
> = rep_list(
'a
;
f
{
n
})
By:
Unab [`rep_list`]
Generated subgoal:
1
<
m
:
. if
m
<
n
then
f
(
m
) else @
x
:
'a
. true
fi ,
n
>
=
<
n@0
:
. if
n@0
<
||
f
{
n
}|| then (
f
{
n
})[
n@0
] else arb(
'a
) fi ,||
f
{
n
}||>
9
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(37steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc