I'm studying Coq's core language and I found that mutual inductive type definition is in it. https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions
Before I read the material, I had supposed that Coq translates mutual definitions in Gallina into nonmutual ones in its core language, since it allows the core language to be smaller. But it wasn't and then I started to wonder why.
odd can be defined mutually as follows.
Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n).
However, one can write another definition without
Inductive even_or_odd: (is_even: bool) -> nat -> Prop := | even_O : even true 0 | even_S : forall n, even false n -> even true (S n) | odd_S : forall n, even true n -> even false (S n). Definition even := even_or_odd true. Definition odd := even_or_odd false.
I agree that the former looks better than the latter. However, What I wonder is if it is always possible to rewrite any mutually defined inductive type in a nonmutual way. If then, Coq does not necessarily include the mutual definition syntax in its core language.
Does the mutual definition allow more expressions to be defined? Is there any mutually defined type that can't be translated to a nonmutual one?
Or there isn't, but my concern about minimal core language is not a big deal?
Also, I am so sure that mutual fixpoints always can be translated to nonmutual ones. It looks much more clear to me compared to the case of inductive definition. Am I right?