I am just getting started with Coq and am confused as to why this isn't allowed.
Inductive prod: Type :=
| pair (n1: nat n2: bool).
I get a "The reference n2 was not found in the current environment" complaint.
When I make both arguments nats, or both arguments bools, like this
Inductive prod: Type :=
| pair (n1 n2: bool).
it doesn't complain.