I was wondering if the order of declarations of an inductive type can matter.
For example in Coq you can define
Nat either by:
Inductive Nat := | O : Nat | S : Nat -> Nat.
Inductive Nat := | S : Nat -> Nat | O : Nat.
This will perhaps change the order of the parameters in the automatically generated eliminator, but that’s not a big deal.
What I’m wondering is if it is possible to write a declaration like
Inductive typewhereordermatters := | cons1 : type1 | cons2 : type2.
type2 is a dependent type, depending on
cons1? (and in this case, write the declarations in the other order would not have any meaning, because
type2 would be referring to
cons1 which does not exists yet).