(6steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mklist
length
T
:Type,
n
:
,
f
:(
n
T
). ||mklist(
n
;
f
)|| =
n
By:
RepeatFor 2 (Analyze 0) THEN NatInd -1 THEN Reduce 0
Generated subgoals:
1
1.
T
: Type
f
:(
0
T
). 0 = 0
Auto
2
1.
T
: Type
2.
n
:
3. 0<
n
4.
f
:(
(
n
-1)
T
). ||mklist(
n
-1;
f
)|| =
n
-1
f
:(
n
T
). ||mklist(
n
;
f
)|| =
n
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
T:Type, n:
, f:(n
T). ||mklist(n;f)|| = n 
T:Type, n:, f:(nT). ||mklist(n;f)|| = n f:(0T). 0 = 0
f:((n-1)T). ||mklist(n-1;f)|| = n-1
f:(nT). ||mklist(n;f)|| = n 
