Re: [isabelle] Type for pairs



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 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.