The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

I have some inductively defined set, say of terms

   Inductive Term : Set := ...

and some inductively defined relation, say of reduction

  Inductive Red : Term -> Term -> Prop := ...

I want to do induction on the size of derivations of the Red relation.
 So I try to define

  Fixpoint RedSize : (M N: Term) (r:Red M N) {struct r} : nat :=
     match r with ...
     end.

This fails, because Red is a Prop, not a Set.  How is this usually done?

One could index the relation Red with size, as is necessary in (simply
typed) HOL, but it seems we should do better with dependent types.

Thanks,
Randy