I recently had a discussion with some of my colleagues about the coding style. Compare
Inductive A :=
 A0 (x:nat): A.
vs:
Inductive A:=
 A0: forall (x:nat), A.
I personally favor the 1st version, for several reasons:

It is terser

It resembles “match” syntax for this type:
match a with
 A0 x => x
end. 
Arguably, it is a bit closer to Haskell and OCaml syntax.

I tend to think about “x” as a “parameter” of a constructor
I am just curious, what is your preference? Why?
Vadim
 Always use forall
 Never use forall
 It depends…
0 voters