Zulip Chat Archive

Stream: new members

Topic: Mutual inductive family


Marcus Rossel (Jul 19 2021 at 10:57):

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?


Last updated: Dec 20 2023 at 11:08 UTC