invalid nested inductive datatype

Stream: new members

[Simon Daniel]

Hi,
i have this Inductive type to capture a sequence of effects:

inductive Free (Eff:Type u → Type v) (α:Type) where
| Do: Eff β → (β → Free Eff α) → Free Eff α
| Return: α → Free Eff α

I now want to define an effect that contains a sequence of effects itself like this:

inductive I: Type -> Type 1 where
| A {a: Type}: Free I a -> I a

which seems to be an invalid nested inductive datatype. I see that i can fix this by moving the Type parameter 'a' to the inductive 'I', but it should be a parameter for the constructor.

[Arthur Adjedj]

Lean doesn't allow for such types. Your best bet would be to define your Free mutually with your effect I:

mutual
  inductive FreeI : Type → Type 1 where
    | Do: I β → (β → FreeI α) → FreeI α
    | Return: α → FreeI α

  inductive I: Type -> Type 1 where
    | A : FreeI a -> I a
end