coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] values for type nat+nat+nat, Tyng-Ruey Chuang
- Re: [Coq-Club] values for type nat+nat+nat,
Pierre Courtieu
- Re: [Coq-Club] values for type nat+nat+nat, Tyng-Ruey Chuang
- Re: [Coq-Club] values for type nat+nat+nat,
Pierre Letouzey
- Re: [Coq-Club] values for type nat+nat+nat, Tyng-Ruey Chuang
- Re: [Coq-Club] values for type nat+nat+nat,
Pierre Courtieu
Archive powered by MhonArc 2.6.16.