The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello

I have the following setup (which follows no intuition but is a
simplified version of the original inductive type reproducing the
effect)

Section T.
Variables (X: Type) (x:X) (A : X -> Prop) (f : forall (x:X), A x -> X -> X).

Inductive AllList X  (P : X -> Prop) : list X -> Prop := 
  empty : AllList _ P nil
| acons : forall x xs , P x -> AllList _ P xs -> AllList _ P (x::xs).

Inductive R : X -> Prop := 
| intro0 : forall x x' a , R (f x a x') -> R x'
| intro1 : forall xs x', AllList _ (fun x => { a : A x | R (f x a x')} ) xs 
-> R x'
| intro2 : R x.

On entering R i get: "Warning: Ignoring recursive call"

1. Question: What does this warning mean and does it have any
consequences on the consistency of the system?

If I remove either intro0 or intro1 (intro2 is just added to not make it
a single constructor inductive proposition) the warning disappears.

2. Question: The above shows that being well-formed (in the sense of no
warnings being issued) is not a property that can be verified in a
rule-by-rule fashion. Can someone explain this?


-- 
Regards
Christian