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.orInductive Nat :=  | S : Nat -> Nat  | O : Nat.This will perhaps change the order of the parameters in the automatically generated eliminator, but thats not a big deal.What Im wondering is if it is possible to write a declaration likeInductive typewhereordermatters :=  | cons1 : type1  | cons2 : type2.where 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).
Does the order of declarations in an inductive type matter?
lo.logic;type theory;coq;dependent type
The order does not matter. I cannot think of a case where it would. As Andrej Bauer points out in a comment, if you change the order the result is canonically isomorphic to the original. One case cannot depend on another case. The elements of the sum represent a choice, so it doesn't make sense that the choice taken depends upon a choice that is not taken.