The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Petar,

you wrote that T can be a list of itself, which justifies this error message. 
Maybe you meant this (which does work):

Record list_singleton (T : Type) := {lT :> list T; cond : length lT = 1}.

Inductive SomeInd (T : Type) :=
 | T_main : list_singleton T -> SomeInd T.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Petar Maksimovic
Sent: Thursday, October 01, 2015 2:28 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Records and Inductive definitions

Any comments? From the developer team, in particular, perhaps? :)

Cheers,
Petar

On 28 September 2015 at 17:27, Petar Maksimovic 
<petar.maksimovic AT gmail.com>
 wrote:
> Hello everyone,
>
> Why is it not possible to do the following in Coq:
>
> Record list_singleton (T : Type) := {lT :> list T; cond : length lT = 1}.
>
> Inductive T : Type :=
>  | T_main : list_singleton T -> T.
>
> It fails with the error message: Error: Non strictly positive 
> occurrence of "T" in "list_singleton T -> T".
>
> I feel that this should be able to go through, since
>
>  | T_main : list T -> T
>
> would go through, and I am simply putting an extra condition on the 
> lists that I allow.
>
> What I would ultimately want is to be able to use Coq's finite maps in 
> constructors, somewhat like this:
>
> Module FMnat := FMapWeakList.Make(Nat_as_OT). (or FMapFullAVL, for 
> that matter)
>
> Definition FMap := FMnat.t.
>
> Inductive T : Type :=
>  | T_main : FMap T -> T.
>
> and I believe that the problem (in this case) boils down to a 
> restriction condition in the underlying record definition of slist, on 
> which FMapWeakList is based, therefore the simplified example above.
>
> Any ideas, including how I could approach this differently, are very 
> appreciated.
>
> Thank you,
> Petar
>
> P.S. The following does not go through:
>
> Inductive T : Type :=
>  | T_main : forall T', list_whatever T T' -> T with Record 
> list_whatever (T T' : Type) := {lT :> list T; whatever : T'}.
>
> with the error message: Error: Cannot handle mutually (co)inductive 
> records, whereas
>
> Record list_whatever (T T' : Type) := {lT :> list T; whatever : T'}.
>
> Inductive T : Type :=
>  | T_main : forall T', list_whatever T T' -> T.
>
> goes through just fine. Why is this so?
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928