<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> </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 <andreas.abel@ifi.lmu.de><br> <b><span style="font-weight: bold;">To:</span></b> Sergei Meshveliani <mechvel@botik.ru> <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>> I do not find a natural access to a tuple field.<br>><br>> 1) Pattern matching does not work in the construct of<br>> ...<br>> where<br>> (_ , _ , z, _) = p<br>><br>> (it needs a more complicated code).<br><br>You could try<br><br> let _ , _ , z , _ = p<br> in ...<br><br>>
2) I wonder of whether I need to use records everywhere for tuples.<br><br>Often, records are preferable since field names offer some natural <br>documentation.<br><br>> 3) Setting to the code the compositions like proj₁ ∘ proj₂ ∘ proj₂<br>> is much less writable and readable than `tuple43'.<br>><br>> So, I define the selectors like<br>><br>> tuple43 : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c}<br>> {D : Set d} →<br>> A × B × C × D → C<br>> tuple43 = proj₁ ∘ proj₂ ∘
proj₂<br>><br>> Am I missing something?<br>> Does Standard library need to include several tuple-ij selectors?<br>><br>> Regards,<br>><br>> ------<br>> Sergei<br>><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><br>-- <br>Andreas Abel <>< 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="{"bundle":{"label_delimitor":":","percentage":"%","smart_buffer":"Smart Buffer","start_playing_when_buffered":"Start playing when buffered","sound":"Sound","desktop_notification":"Desktop Notification","continuation_on_next_line":"-","loop":"Loop","only_notify":"Only
Notify","estimated_time":"Estimated Time","global_preferences":"Global Preferences","no_notification_supported_on_your_browser":"No notification style supported on your browser version","video_buffered":"Video Buffered","buffered":"Buffered","hyphen":"-","buffered_message":"The video has been buffered as requested and is ready to play.","not_supported":"Not Supported","on":"On","off":"Off","click_to_enable_for_this_site":"Click to enable for this site","desktop_notification_denied":"You have denied permission for desktop notification for this site","notification_status_delimitor":";","error":"Error","adblock_interferance_message":"Adblock (or similar
extension) is known to interfere with SmartVideo. Please add this url to adblock whitelist.","calculating":"Calculating","waiting":"Waiting","will_start_buffering_when_initialized":"Will start buffering when initialized","will_start_playing_when_initialized":"Will start playing when initialized","completed":"Completed","buffering_stalled":"Buffering is stalled. Will stop.","stopped":"Stopped","hr":"Hr","min":"Min","sec":"Sec","any_moment":"Any Moment","page_action_title_enabled":"Loop (enabled)","page_action_title_disabled":"Loop
(disabled)"},"tabId":"dadb5c75-cac7-2905-65ae-e291d1f7fdce","prefs":{"desktopNotification":true,"soundNotification":true,"logLevel":0,"enable":true,"loop":false,"hidePopup":false,"autoPlay":false,"autoBuffer":false,"autoPlayOnBuffer":false,"autoPlayOnBufferPercentage":42,"autoPlayOnSmartBuffer":true,"quality":"hd720","fshd":true,"onlyNotification":false,"enableFullScreen":true,"saveBandwidth":true,"hideAnnotations":false,"turnOffPagedBuffering":true}}"></mytubeelement><mytubeelement id="myTubeRelayElementToTab" event="relayPrefs" data="{"loadBundle":true}"></mytubeelement></div></body></html>