coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Records and Inductive definitions
- Date: Thu, 1 Oct 2015 15:22:13 +0200
On 01/10/2015 15:12, Petar Maksimovic wrote:
> I think that the length condition that I had (length lT = 1) is
> causing the issue, but I don't quite understand why.
Indeed, the problem is that the length mentions the type T, and not in a
strictly positive fashion, because length is essentially a fixpoint. The
manual describes what it means to be strictly positive here:
https://coq.inria.fr/refman/Reference-Manual006.html#sec199
As you can see, it is a syntactical approximation to ensure
productivity, and in particular it is only an under-approximation. Your
use case is perfectly sound semantically but not syntactically positive.
In your use case, you can workaround this limitation by using vectors
(which won't lack an occasion to make you regret to use them), in the
following way:
Require Vector.
Inductive T : Type :=
| T_main : Vector.t T 1 -> T.
The Vector.t type encodes in a positive fashion what you were looking
for. Yet, you're probably going to suffer if you wish to write dependent
programs.
Good luck,
PMP
Attachment:
signature.asc
Description: OpenPGP digital signature
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Pierre-Marie Pédrot, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Epiphanie, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/05/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
Archive powered by MHonArc 2.6.18.