[Agda] tuple selectors
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Aug 12 14:39:53 CEST 2013
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/
More information about the Agda
mailing list