<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Or you could use `with`</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>... with p</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>... | _ , _ , z , _ = ...</span></div><div></div><div>&nbsp;</div><div>- darryl</div><div><br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1">  <font
 size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Andreas Abel &lt;andreas.abel@ifi.lmu.de&gt;<br> <b><span style="font-weight: bold;">To:</span></b> Sergei Meshveliani &lt;mechvel@botik.ru&gt; <br><b><span style="font-weight: bold;">Cc:</span></b> agda@lists.chalmers.se <br> <b><span style="font-weight: bold;">Sent:</span></b> Monday, August 12, 2013 8:39 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] tuple selectors<br> </font> </div> <div class="y_msg_container"><br>On 12.08.2013 09:56, Sergei Meshveliani wrote:<br>&gt; I do not find a natural access to a tuple field.<br>&gt;<br>&gt; 1) Pattern matching does not work in the construct of<br>&gt;&nbsp; &nbsp;  ...<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; where<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; (_ , _ , z, _) = p<br>&gt;<br>&gt; (it needs a more complicated code).<br><br>You could try<br><br>&nbsp;  let _ , _ , z , _ = p<br>&nbsp;  in&nbsp; ...<br><br>&gt;
 2) I wonder of whether I need to use&nbsp; records&nbsp; everywhere for tuples.<br><br>Often, records are preferable since field names offer some natural <br>documentation.<br><br>&gt; 3) Setting to the code the compositions like&nbsp; proj₁ ∘ proj₂ ∘ proj₂<br>&gt;&nbsp; &nbsp;  is much less writable and readable than&nbsp; `tuple43'.<br>&gt;<br>&gt; So, I define the selectors like<br>&gt;<br>&gt;&nbsp; &nbsp; tuple43 : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c}<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; {D : Set d} →<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;  A × B × C × D → C<br>&gt;&nbsp; &nbsp; tuple43 = proj₁ ∘ proj₂ ∘
 proj₂<br>&gt;<br>&gt; Am I missing something?<br>&gt; Does Standard library need to include several&nbsp; tuple-ij&nbsp; selectors?<br>&gt;<br>&gt; Regards,<br>&gt;<br>&gt; ------<br>&gt; Sergei<br>&gt;<br>&gt; _______________________________________________<br>&gt; Agda mailing list<br>&gt; <a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>&gt;<br><br><br>-- <br>Andreas Abel&nbsp; &lt;&gt;&lt;&nbsp; &nbsp; &nbsp; Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>Oettingenstr. 67, D-80538 Munich, GERMANY<br><br><a ymailto="mailto:andreas.abel@ifi.lmu.de" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br><a href="http://www2.tcs.ifi.lmu.de/~abel/"
 target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br></div> </div> </div>  <mytubeelement id="myTubeRelayElementToPage" event="preferencesUpdated" data="{&quot;bundle&quot;:{&quot;label_delimitor&quot;:&quot;:&quot;,&quot;percentage&quot;:&quot;%&quot;,&quot;smart_buffer&quot;:&quot;Smart Buffer&quot;,&quot;start_playing_when_buffered&quot;:&quot;Start playing when buffered&quot;,&quot;sound&quot;:&quot;Sound&quot;,&quot;desktop_notification&quot;:&quot;Desktop Notification&quot;,&quot;continuation_on_next_line&quot;:&quot;-&quot;,&quot;loop&quot;:&quot;Loop&quot;,&quot;only_notify&quot;:&quot;Only
 Notify&quot;,&quot;estimated_time&quot;:&quot;Estimated Time&quot;,&quot;global_preferences&quot;:&quot;Global Preferences&quot;,&quot;no_notification_supported_on_your_browser&quot;:&quot;No notification style supported on your browser version&quot;,&quot;video_buffered&quot;:&quot;Video Buffered&quot;,&quot;buffered&quot;:&quot;Buffered&quot;,&quot;hyphen&quot;:&quot;-&quot;,&quot;buffered_message&quot;:&quot;The video has been buffered as requested and is ready to play.&quot;,&quot;not_supported&quot;:&quot;Not Supported&quot;,&quot;on&quot;:&quot;On&quot;,&quot;off&quot;:&quot;Off&quot;,&quot;click_to_enable_for_this_site&quot;:&quot;Click to enable for this site&quot;,&quot;desktop_notification_denied&quot;:&quot;You have denied permission for desktop notification for this site&quot;,&quot;notification_status_delimitor&quot;:&quot;;&quot;,&quot;error&quot;:&quot;Error&quot;,&quot;adblock_interferance_message&quot;:&quot;Adblock (or similar
 extension) is known to interfere with SmartVideo. Please add this url to adblock whitelist.&quot;,&quot;calculating&quot;:&quot;Calculating&quot;,&quot;waiting&quot;:&quot;Waiting&quot;,&quot;will_start_buffering_when_initialized&quot;:&quot;Will start buffering when initialized&quot;,&quot;will_start_playing_when_initialized&quot;:&quot;Will start playing when initialized&quot;,&quot;completed&quot;:&quot;Completed&quot;,&quot;buffering_stalled&quot;:&quot;Buffering is stalled. Will stop.&quot;,&quot;stopped&quot;:&quot;Stopped&quot;,&quot;hr&quot;:&quot;Hr&quot;,&quot;min&quot;:&quot;Min&quot;,&quot;sec&quot;:&quot;Sec&quot;,&quot;any_moment&quot;:&quot;Any Moment&quot;,&quot;page_action_title_enabled&quot;:&quot;Loop (enabled)&quot;,&quot;page_action_title_disabled&quot;:&quot;Loop
 (disabled)&quot;},&quot;tabId&quot;:&quot;dadb5c75-cac7-2905-65ae-e291d1f7fdce&quot;,&quot;prefs&quot;:{&quot;desktopNotification&quot;:true,&quot;soundNotification&quot;:true,&quot;logLevel&quot;:0,&quot;enable&quot;:true,&quot;loop&quot;:false,&quot;hidePopup&quot;:false,&quot;autoPlay&quot;:false,&quot;autoBuffer&quot;:false,&quot;autoPlayOnBuffer&quot;:false,&quot;autoPlayOnBufferPercentage&quot;:42,&quot;autoPlayOnSmartBuffer&quot;:true,&quot;quality&quot;:&quot;hd720&quot;,&quot;fshd&quot;:true,&quot;onlyNotification&quot;:false,&quot;enableFullScreen&quot;:true,&quot;saveBandwidth&quot;:true,&quot;hideAnnotations&quot;:false,&quot;turnOffPagedBuffering&quot;:true}}"></mytubeelement><mytubeelement id="myTubeRelayElementToTab" event="relayPrefs" data="{&quot;loadBundle&quot;:true}"></mytubeelement></div></body></html>