Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Type for pairs


view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

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

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: Eg Gloor <egglue@gmail.com>
I've found a solution: use Cartesian product instead.

Thanks
Eg

view this post on Zulip Email Gateway (Aug 18 2022 at 15:46):

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

view this post on Zulip Email Gateway (Aug 18 2022 at 15:47):

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
Eg

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

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

datatype ('a, 'b) graph = Graph 'a 'b

which is already present with the product type.

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP 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