blob: 4764037d941832ec36cea4d8689553f7a5681a4f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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.
|
