Skip to Content.
Sympa Menu

coq-club - [Coq-Club] values for type nat+nat+nat

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] values for type nat+nat+nat


chronological Thread 
  • From: Tyng-Ruey Chuang <trc AT iis.sinica.edu.tw>
  • To: coq-club AT pauillac.inria.fr
  • Cc: trc AT iis.sinica.edu.tw
  • Subject: [Coq-Club] values for type nat+nat+nat
  • Date: Wed, 01 Oct 2003 14:53:16 +0800
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page