From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- contrib/subtac/test/measure.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 contrib/subtac/test/measure.v (limited to 'contrib/subtac/test/measure.v') diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v new file mode 100644 index 00000000..4764037d --- /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 -- cgit v1.2.3