diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-22 08:51:24 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-22 08:51:24 +0000 |
commit | 0f03185388e6d4d2ac376e2e8120437a6ae471b7 (patch) | |
tree | f8bf36daa73b81671cabfc0b7909e40bcfa23959 /contrib/subtac/test/measure.v | |
parent | a581a7ba67cf3fadb2f80db0f0174cd385162bd6 (diff) |
Mutually structurally recursive defs and rec using measures added.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/test/measure.v')
-rw-r--r-- | contrib/subtac/test/measure.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v new file mode 100644 index 000000000..4764037d9 --- /dev/null +++ b/contrib/subtac/test/measure.v @@ -0,0 +1,24 @@ +Notation "( x & y )" := (@existS _ _ x y) : core_scope. +Unset Printing All. +Require Import Coq.Arith.Compare_dec. + +Require Import Coq.subtac.Utils. + +Fixpoint size (a : nat) : nat := + match a with + 0 => 1 + | S n => S (size n) + end. + +Program Fixpoint test_measure (a : nat) {measure a size} : nat := + match a with + | S (S n) => S (test_measure n) + | x => x + end. +subst. +unfold n0. +auto with arith. +Qed. + +Check test_measure. +Print test_measure.
\ No newline at end of file |