1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(* Examples to check that the guard condition does not evaluate
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.
Fixpoint slow2 n :=
match n with
| 0 => 0
| S k => slow2 k + slow2 k
end.
Timeout 5 Time Fixpoint F' n :=
match n with
| 0 => 0
| S k =>
if slow2 100 then F' k else 0
end.
|
