The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Thank you Vincent.  My eyes were crossed from too much Coq.

Best,
Randy
--
On Thu, Sep 22, 2011 at 3:13 AM, Vincent Siles
<vincent.siles AT ens-lyon.org>
 wrote:
> I'm not on a computer with Coq installed right now (what a shame, I
> know), but if this is an
> exact copy/paste of your problem, I guess the : just after fmlaFV is
> the problem.
> What's happening if you remove it ?
>
> Best,
> Vincent
>
> 2011/9/22 Randy Pollack 
>Â <rpollack0 AT gmail.com>:
>> What does this error message mean?  Consider the following code in Coq 
>> 8.3pl2:
>>
>> =======
>> Reset Initial.
>> Set Implicit Arguments.
>>
>> Inductive sort : Set := Name | Lam.
>> Definition var := (prod nat sort).
>>
>> Inductive trm : sort -> Set :=
>> | ivar : forall (x:var), trm (snd x)
>> | aply : forall (K:trm Lam) (M:trm Lam), trm Lam.
>>
>> Fixpoint trmFV (s:sort) (X:trm s) {struct X} : list var :=
>>  match X with
>>    | ivar x => cons x nil
>>    | aply K M => app (trmFV K) (trmFV M)
>>  end.
>>
>> Inductive fsort : Set := prop | aprop.
>>
>> Inductive fmla : fsort -> Set :=
>> | feq: forall (s:sort) (t u: trm s), fmla prop
>> | fand: forall (P Q:fmla prop), fmla prop.
>>
>> Fixpoint fmlaFV: (fs:fsort) (X:fmla fs) {struct X} : list var :=
>>  match X with
>>    | feq t u => app (trmFV t) (trmFV u)
>>    | fand P Q => app (fmlaFV P) (fmlaFV Q)
>>  end.
>> =====
>>
>> The definition of termFV (free variables in a term) is accepted, but
>> the definition of fmlaFV (free variables in a formula) is rejected
>> with the error message above.  I don't see the problem.
>>
>> Thanks for any help.
>> Randy
>>
>