The Coq mailing list

[Michael Shulman <viritrilbia AT gmail.com>]

Hi,

The following code (a simplification) defines a family of list types
indexed by the natural numbers (the index has nothing to do with the
length of the list or anything else).  My attempt to define a function
which decrements the list index is refused by the termination checker.
Why is it confused, and what can I do to persuade it that the function
does terminate?

Thanks!
Mike


Section mylist.

  Parameter A:Type.

  Inductive mylist : nat -> Type :=
  | mynil : forall n:nat, mylist n
  | mycons : forall n:nat, A -> mylist n -> mylist n.

  Fixpoint declabel (n:nat)(xs : mylist (S n)) {struct xs} : mylist n :=
    match xs in mylist Sn return mylist (pred Sn) with
      | mynil _ => mynil _
      | mycons O x xs' => mynil _
      | mycons (S n) x xs' => mycons x (declabel xs')
    end.

End mylist.