mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
:
,
f
:(
n
T
). ||mklist(
n
;
f
)|| =
n
[mklist_length]
cites the following:
Thm*
as
,
bs
:
T
List. ||
as
@
bs
|| = ||
as
||+||
bs
||
[length_append]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc
n:
, f:(n
T). ||mklist(n;f)|| = n 
as,bs:T List. ||as @ bs|| = ||as||+||bs|| n:, f:(nT). ||mklist(n;f)|| = n as,bs:T List. ||as @ bs|| = ||as||+||bs||