I recently had a discussion with some of my colleagues about the coding style. Compare
Inductive A :=
| A0 (x:nat): 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
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?
- Always use forall
- Never use forall
- It depends…