From: Eg Gloor <egglue@gmail.com>
Hello,
I'm trying to define a type for representing a graph and think a type for a
pair of functions would be suitable. How do I do that? I've tried
datatype graph = "('a, 'b)"
But then
consts
grph1 :: graph
a :: "nat => nat"
b :: "nat => nat"
...
"grph1 = (a x, b x)" as an axiom complains about clash of types "*" and
"graph". I must be doing something wrong here.
Thanks for the help.
Eg
From: Eg Gloor <egglue@gmail.com>
I've found a solution: use Cartesian product instead.
Thanks
Eg
From: Eg Gloor <egglue@gmail.com>
Hi,
Just a question on top of an old question: Do you know how the first element
of a pair can be retrieved if it was represented as a pair? Is there
something like 'fst'?
Thanks
Eg
From: Tobias Nipkow <nipkow@in.tum.de>
Eg Gloor wrote:
Hi,
Just a question on top of an old question: Do you know how the first element
of a pair can be retrieved if it was represented as a pair? Is there
something like 'fst'?
There is "fst". And "snd".
Tobias
Thanks
EgOn Mon, Aug 2, 2010 at 1:37 AM, Eg Gloor <egglue@gmail.com> wrote:
Hi Florian,
Just a question on an old question: Do you know how the first element of a
pair can be retrieved if it was represented as a pair? Is there something
like 'fst'?Thanks
EgOn Mon, Jun 7, 2010 at 7:31 AM, Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de> wrote:
Hi Eg,
datatype graph = "('a, 'b)"
using this you have defined a datatype with one singleton constructor
named "('a, 'b)". What you had in mind was something likedatatype ('a, 'b) graph = Graph 'a 'b
which is already present with the product type.
Hope this helps,
Florian--
Home:
http://www.in.tum.de/~haftmannPGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Last updated: Mar 29 2024 at 12:28 UTC