Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Non strictly positive occurrence in constructor

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Non strictly positive occurrence in constructor


chronological Thread 
  • From: Damien Pous <Damien.Pous AT ens-lyon.fr>
  • To: ben <Benedikt.Ahrens AT unice.fr>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Non strictly positive occurrence in constructor
  • Date: Tue, 8 Jun 2010 15:01:31 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=AxlBwD9wj3gjA7/qiAuj3ygaqvkg+PBwVYBZJrugsFAQAfyteya4Timz1lM4BEi5BY /qTI1w7k2SYLDR5yPeunQ45MHxvtPkXZstsDBVV88NcgecQOUYNThiY5x51DfoFrHs4P vCW9QbXqrklgoY6aDDi6T0NQWek8TD6+BGe70=

Maybe you could replace the fixpoint with an inductive (I hope I
didn't swap indices...) ?

Inductive vect X: nat -> Type :=
| vnil: vect X O
| vcons: forall n, X -> vect X n -> vect X (S n).

Inductive type: nat -> Type :=
 | constr : forall n k, vect (type n) k -> type (S n).

Hope this helps,
Damien



2010/6/8 ben 
<Benedikt.Ahrens AT unice.fr>:
> Dear all,
>
> I run into a "non strictly positive occurrence" in a situation which is
> similar to the following simplified example:
>
> ============================
>
> Fixpoint n_prod (X : Type) (n : nat) : Type :=
>  match n with
>  | O => unit
>  | S n => prod X (n_prod X n)
>  end.
>
>
> Inductive type : nat -> Type :=
>  | constr : forall n k,
>        (n_prod (type n) k) -> type (S n).
>
> ============================
>
>
> Is there an "equivalent definition" which would be accepted by Coq?
>
> Thanks
> Benedikt
>
>
>




Archive powered by MhonArc 2.6.16.

Top of Page