blob: 387263e2f3da9e7252d76730a4de2d8edd0f1fa2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Examples to check that the guard condition does not unfold
irrelevant subterms *)
(* Expected time < 1.00s *)
Require Import Bool.
Fixpoint slow n :=
match n with
| 0 => true
| S k => andb (slow k) (slow k)
end.
Timeout 5 Time Fixpoint F n :=
match n with
| 0 => 0
| S k =>
if slow 100 then F k else 0
end.
|
