baz_num_elts exercise from Software Foundations
-
31-10-2019 - |
Question
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 baz
because 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 x
or y
. We can't get a value of type baz
without already having a value of type baz
.
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 true
and false
. Under this interpretation, I would argue that there are zero elements of type baz
.
Am I correct, or can someone explain what I'm misunderstanding?
No correct solution