The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

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?