The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> This leaves open the question of what should happen with "nested" 
types, like:

I would say it's more a question about non recursively uniform 
parameters than about nesting

For instance x in [Acc R x := Acc_intro : (forall y, R y x -> Acc R y) 
-> Acc R x]

Gaëtan Gilbert

On 26/08/2019 15:06, Stefan Monnier wrote:
> > I'm not an expert but a very sutil interpretation of the rules seems that
> > the nested positive condition should be applied only considering the arity
> > of the inductives without the parameters as if the `List (Rose A)` would be
> > a new inductive.
>
> BTW, this makes a lot of sense if you consider that in the literature,
> the CIC is usually presented in such a way that parameters are *outside*
> of the inductive definition.  IOW
>
>      Inductive Rose (A : Set) : Set :=
>      | rose : (List (Rose A)) -> Rose A.
>
> isn't encoded as
>
>      Rose = Ind(self: Set → Set)
>                < rose : (List (self A)) -> self A >
>
> but as
>
>      Rose = λ (A : Set) . Ind(self: Set)
>                           < rose : (List self) -> self >
>
> This leaves open the question of what should happen with "nested" types, like:
>
>      Inductive Rose (A : Set) : Set :=
>      | rose : (List (Rose (List A))) -> Rose A.
>
> which can't be encoded this way, yet is accepted (i.e. the arg is
> considered as a parameter and not as an index).
>
>
>          Stefan