The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT univ-orleans.fr>]

Hello,

Values of type nat+nat are for example:

(inl nat nat O)
(inr nat nat O)

Values of type nat + (nat+nat) are for example:

(inl nat (nat+nat) O).

(inr nat (nat+nat) (inl nat nat O))

(inr nat (nat+nat) (inr nat nat O))

Cheers,

Pierre


Tyng-Ruey Chuang 
<trc AT iis.sinica.edu.tw>
 wrote:
> 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
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>