The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Fri, Apr 20, 2012 at 11:25:04PM -0400, Vilhelm Sjöberg wrote:
> 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))).
>

Thanks - it looks obious now I've seen it!

Bernard