diff options
Diffstat (limited to 'plugins/subtac/test/measure.v')
-rw-r--r-- | plugins/subtac/test/measure.v | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v deleted file mode 100644 index 4f938f4f..00000000 --- a/plugins/subtac/test/measure.v +++ /dev/null @@ -1,20 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.Program.Program. - -Fixpoint size (a : nat) : nat := - match a with - 0 => 1 - | S n => S (size n) - end. - -Program Fixpoint test_measure (a : nat) {measure size a} : nat := - match a with - | S (S n) => S (test_measure n) - | 0 | S 0 => a - end. - -Check test_measure. -Print test_measure.
\ No newline at end of file |