The Coq mailing list

["Hao-yang Wang" <hywang AT pobox.com>]

Hi! Could somebody please point to me why I would get the error
'Recursive call to T has principal argument equal to "x" instead of xs'
with the following definitions? Aren't both "x" and "xs" subterms of "l"?

Thanks,
Hao-yang Wang


Require Import List.

Inductive term (V F:Set): Set :=
    | Var: V -> term V F
    | App: F -> list (term V F) -> term V F.

Definition term_ind2 (V F:Set) (P: term V F->Prop) (PL: list (term V
F)->Prop)
          (* term *) (tv: forall v, P (Var V F v))
                     (ta: forall f ts, PL ts -> P (App V F f ts))
     (* term list *) (lz: PL nil)
                     (ls: forall x, (P x) -> forall xs, PL xs -> PL (x::xs))
:=
fix T (t: term V F): P t :=
    match t return P t with
    | Var v => tv v
    | App f ts => ta f ts (TL ts)
    end
with TL (l: list (term V F)): PL l :=
    match l return PL l with
    | nil => lz
    | x::xs => ls x (T x) xs (TL xs)
    end
for T.