diff options
author | 2010-03-11 19:08:46 +0000 | |
---|---|---|
committer | 2010-03-11 19:08:46 +0000 | |
commit | dba2ae9fa1eb01d795d36b209aee6045967ba00a (patch) | |
tree | e8c2ce9a5fb8f7a0150458d7a2a5a585ccdca2f9 /test-suite | |
parent | 8a944fd93df07453cba53b752670ae451c370a65 (diff) |
introduced lazy computation of size info in the guard condition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12862 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/complexity/guard.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v new file mode 100644 index 000000000..f64ffc259 --- /dev/null +++ b/test-suite/complexity/guard.v @@ -0,0 +1,17 @@ +(* Examples to check that the guard condition does not unfold + irrelevant subterms *) +(* Expected time < 1s *) +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. |