(6steps total)
PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hel
wd
2
1.
'a
: S
2.
l
: hlist(
'a
)
3.
n
:
el(
n
+1,
l
) = el(
n
,tl(
l
))
By:
RW (NthC 1 (RecUnfoldTopC `hel`)) 0 THEN Simp THEN StrongAuto
Generated subgoal:
1
if
n
+1=
0 then hd(
l
) else el(
n
+1-1,tl(
l
)) fi = el(
n
,tl(
l
))
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
el(n+1,l) = el(n,tl(l))
el(n+1,l) = el(n,tl(l)) if n+1=
0 then hd(l) else el(n+1-1,tl(l)) fi = el(n,tl(l))
