Mutual inductive family

Stream: new members

[Marcus Rossel]

I'm trying to define two inductive families which depend on each other for each "family-index step":

universe u

mutual inductive network, reactor
with network : ℕ → Type u
| empty : network 0
| mk : ∀ d, list (reactor (d - 1)) → network d
with reactor : ℕ → Type u
| mk : ∀ d, network d → reactor d

That is:

• network 0 should be constructible from empty
• network (succ n) should be constructible from list (reactor n)
• reactor n should be constructible from network n

The definition above produces the error:

nested occurrence 'list.{u} (reactor.{u} (has_sub.sub.{0} nat nat.has_sub d (has_one.one.{0} nat nat.has_one)))' contains variables that are not parameters

I'm guessing this means that I can't write the d - 1.
Can I define this in a way that constrains the second constructor to d = succ n for some n : ℕ, so that I can then say:

| mk : list (reactor n) → network d

Or more generally: Is this even correct syntax?