23 lines
399 B
Coq
23 lines
399 B
Coq
Section FOR.
|
|
Variable T : Type.
|
|
Variable body : nat -> T -> T.
|
|
Variable start : nat.
|
|
|
|
Fixpoint for_loop n : T -> T :=
|
|
match n with
|
|
| O => fun s => s
|
|
| S n' => fun s => for_loop n' (body (start + n') s)
|
|
end.
|
|
|
|
End FOR.
|
|
|
|
Eval vm_compute in
|
|
for_loop _
|
|
(fun i =>
|
|
cons
|
|
(for_loop _
|
|
(fun j => cons tt)
|
|
0 (S i) nil
|
|
)
|
|
)
|
|
0 5 nil.
|