The Coq mailing list

[Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>]

On 2012-04-20 23:13, Bernard Hurley wrote:
> 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?


Definition foo : vstack (Nat :: Bool :: Nat :: nil)
  := (2, (true, (7, tt))).

Vilhelm Sjöberg