The Coq mailing list

[Tyng-Ruey Chuang <trc AT iis.sinica.edu.tw>]

Hi,

Here comes a question from a novice:

        What is the syntax for creating and destructing values
        of type nat+nat+nat ?

For nat+nat, there are inl and inr predefined in the Standard Library.
(I assume nat+nat is the shorthand for (sum nat nat))

It seems to be that Coq toplevel understands type nat+nat+nat,
which is different from nat+(nat+nat), but I cannot find Coq syntax
to construct and desctruct values of this types.

Sorry if this a FAQ. Thanks in advance.

best,
Tyng-Ruey Chuang