<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>You really ought to give an example where this distinction makes a difference.</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> Jonathan Leivent <jleivent@comcast.net><br> <b><span style="font-weight: bold;">To:</span></b> agda@lists.chalmers.se <br> <b><span style="font-weight: bold;">Sent:</span></b> Sunday, August 25, 2013 1:45 PM<br> <b><span style="font-weight: bold;">Subject:</span></b> [Agda] rewriting product types vs. single ctor data/record types<br> </font> </div> <div class="y_msg_container"><br>I had thought that
a type like<br><br>Σ[ a ∈ A ] Σ[ b ∈ B ] Σ[c ∈ C ] (D a b c)<br><br>wouldn't be any easier to use - and actually less "nice" than its <br>fully-named counterpart:<br><br>record DR : Set _ where<br> field<br> a : A<br> b : B<br> c : C<br> d : D a b c<br><br>or a similar single ctor inductive data type. However, the (dependent) <br>product type seems more rewritable: if you have just "DR" as a goal, <br>you can't use rewrite to help you fit things into its fields; but if you <br>have that messy (dependent) product, the types of the fields (A, B, C) <br>are part of the type itself - hence visible in the goal - and so can be <br>targeted by rewriting.<br><br>Is there a way around this? Is there some way to rewrite "into" the <br>fields of a data/record type that appears as a goal, to achieve the same <br>effect as rewriting would on a very similar product
type?<br><br>-- Jonathan<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":"85a345fc-806a-f0e2-3bf6-62587424227e","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>