(17steps total)
PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hcons
def
1
2
1
1
1
1
1.
'a
: S
2.
h
:
'a
3.
t
: hlist(
'a
)
4.
n
:
5.
n
<||
t
||+1
6.
n
= 0
cons(
h
;
t
)[
n
] =
h
'a
By:
L
Thm*
a
:
T
,
as
:
T
List,
i
:
.
i
0
cons(
a
;
as
)[
i
] =
a
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(17steps total)
PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
cons(h; t)[n] = h 
'a
a:T, as:T List, i:
. i
0 
cons(a; as)[i] = a
