Re: [isabelle] Type for pairs



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

On Mon, Aug 2, 2010 at 1:37 AM, Eg Gloor <egglue at 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 at 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
>>
>>
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.