The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi,

I have a feeling this question might have an obvious answer, but I can't
see what it is!

After this code, which is adapted from Adam Chlipala's book:

++++++++++++++++++++++++++++++++++++++++

Inductive type : Set := Nat | Bool.

Definition tstack := list type.

Definition typeDenote (t : type) : Set :=
  match t with
    | Nat => nat
    | Bool => bool
  end.

Fixpoint vstack (ts : tstack) : Set :=
  match ts with
    | nil => unit
    | t :: ts' => typeDenote t * vstack ts'
  end%type.

++++++++++++++++++++++++++++++++++++++++

it seems logical to me that one ought to be able to construct an object
of data type  [vstack (Nat :: Bool :: Nat :: nil)] that corresponds in
the "obvious" way to the sequence (2, true, 7). However I can't see how
this could be done. How could it be done?

Regards,

Bernard.