I'm at the following exercise in Software Foundations:
(** **** Exercise: 2 stars (baz_num_elts) *) (** Consider the following inductive definition: *) Inductive baz : Type := | x : baz -> baz | y : baz -> bool -> baz. (** How _many_ elements does the type [baz] have? (* FILL IN HERE *)  *)
All of the answers I've seen on the Internet say that the answer is 2, and that the elements are x and y. If that's the case, then it's not clear to me what is meant by elements. There are certainly two constructors, but it's impossible to actually create a value of type baz.
It's impossible to create a value of type
x has type
baz -> baz.
y has type
baz -> bool -> baz. In order to get a value of type
baz we need to pass a value of type
baz to either
y. We can't get a value of type
baz without already having a value of type
So far I've been interpreting elements to mean values. So
(cons nat 1 nil) and
(cons nat 1 (cons nat 2 nil)) would both be elements of type
list nat and there would be an infinite number of elements of type
list nat. There would be two elements of type
bool, which are
false. Under this interpretation, I would argue that there are zero elements of type
Am I correct, or can someone explain what I'm misunderstanding?