blob: 6a5e9a4023cc4e2a05be9b9ceb9df9889b5d157e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Fixpoint stupid (n : nat) : unit :=
match n with
| 0 => tt
| S n =>
let () := stupid n in
let () := stupid n in
tt
end.
Goal True.
Proof.
pose (v := stupid 24).
Timeout 2 vm_compute in v.
exact I.
Qed.
|