1
Notation "( x & y )" := (@existS _ _ x y) : core_scope.
3
Require Import Coq.Arith.Compare_dec.
5
Require Import Coq.Program.Program.
7
Fixpoint size (a : nat) : nat :=
13
Program Fixpoint test_measure (a : nat) {measure size a} : nat :=
15
| S (S n) => S (test_measure n)
b'\\ No newline at end of file'