The Coq mailing list

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

Thanks! But the problem is that nat+nat+nat is not the same as nat+(nat+nat)
in Coq. As an evidence, try the following in the Coq toplevel:

     Definition k: nat+nat+nat := (inr nat (nat+nat) (inr nat nat O)).

One gets the following error message in return:

     Error: The term (inr nat nat+nat (inr nat nat O)) has type
      nat+(nat+nat) while it is expected to have type nat+nat+nat

So, how does one express a value of type nat+nat+nat (which is 
builtin in Coq)?

best,
Tyng-Ruey


Pierre Courtieu wrote:

> 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
> >
> >    
>
>