[Agda] tuple selectors

[Darryl McAdams]

Or you could use `with`

... with p
... | _ , _ , z , _ = ...
 
- darryl


________________________________
 From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Sergei Meshveliani <mechvel at botik.ru> 
Cc: agda at lists.chalmers.se 
Sent: Monday, August 12, 2013 8:39 AM
Subject: Re: [Agda] tuple selectors
 

On 12.08.2013 09:56, Sergei Meshveliani wrote:
> I do not find a natural access to a tuple field.
>
> 1) Pattern matching does not work in the construct of
>     ...
>        where
>        (_ , _ , z, _) = p
>
> (it needs a more complicated code).

You could try

   let _ , _ , z , _ = p
   in  ...

> 2) I wonder of whether I need to use  records  everywhere for tuples.

Often, records are preferable since field names offer some natural 
documentation.

> 3) Setting to the code the compositions like  proj₁ ∘ proj₂ ∘ proj₂
>     is much less writable and readable than  `tuple43'.
>
> So, I define the selectors like
>
>    tuple43 : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c}
>                                                  {D : Set d} →
>                                                         A × B × C × D → C
>    tuple43 = proj₁ ∘ proj₂ ∘ proj₂
>
> Am I missing something?
> Does Standard library need to include several  tuple-ij  selectors?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130812/ead2ba29/attachment.html