<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
thank you. indeed that is the trick.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/" style="">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank" style=""></a></b></span></span></font></div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of James Wood <james.wood.100@strath.ac.uk><br>
<b>Sent:</b> November 5, 2019 4:41 PM<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] copattern split in Emacs?</font>
<div> </div>
</div>
<div>
<p>Hi Jason,</p>
<p><br>
</p>
<p>If I understand the question correctly, it's the usual C-c C-c for case-splitting, but on an empty hole and followed immediately by RET, rather than entering a variable name. The intermediate prompt is “pattern variables to case (empty for split on result)”.
It's splitting on the result that you want.<br>
</p>
<p><br>
</p>
<p>Regards,</p>
<p>James</p>
<p><br>
</p>
<div class="x_moz-cite-prefix">On 05/11/2019 21:14, Jason -Zhong Sheng- Hu wrote:<br>
</div>
<blockquote type="cite"><style type="text/css" style="display:none">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Hi all,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
is there a key stroke for copattern split? I looked up the docs and it seems not, right?<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_Signature">
<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/" style="">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet
ms,sans-serif"></span></span></font></div>
</div>
<br>
<fieldset class="x_mimeAttachmentHeader"></fieldset>
<pre class="x_moz-quote-pre">_______________________________________________
Agda mailing list
<a class="x_moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="x_moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</div>
</body>
</html>