The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.jussieu.fr>]

Hi,
Le 19 sept. 11 à 08:39, Levis John a écrit :

> Now i want to define GroundTerms, a subset of Term, in which terms  
> have no free variables:
>
> Inductive GroundTerm:Term->Prop:=
> |FuncApp_GroundTerm:forall (func:Function L)(ts : Terms  
> (arityFunction L func)),
>     GroundTerms (arityFunction L func) ts -> GroundTerm (FunApp func  
> ts)
>
> |Tnil_GroundTerms:GroundTerms 0 Tnil
> |Tcons_GroundTerms:forall(n:nat)(t:Term)(ts:Terms n),
>   GroundTerm t ->GroundTerms n ts-> GroundTerms (S n) (Tcons n t ts).
>
> The GoundTerm definition makes sense to me, but the Coq complains  
> that Parameters should be
> syntactically the same for GroundTerm and GroundTerms.
>
> Any suggestions?
> ............
Coq complains because n is a parameter of GroundTerms and not of  
GroundTerm but look : n isn't a parameter at all
 - Tnil_GroundTerms returns GroundTerms 0 ... and not GroundTerms n ...
 - Tcons_GroundTerms GroundTerms (S n) ... instead of GroundTerms  
n ... .

So just define n as an argument thanks to
+ with GroundTerms : forall (n:nat), (Terms n)->Prop:=
and you'll be fine

if you don't understand why the : place changes everything you can
 - try to fight http://coq.inria.fr/refman/Reference-Manual006.html#toc31
 - read http://adam.chlipala.net/cpdt/html/InductiveTypes.html
 ;-)

All the best,
Pierre Boutillier