<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
</head>
<body>
<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="moz-cite-prefix">On 05/11/2019 21:14, Jason -Zhong Sheng- Hu wrote:<br>
</div>
<blockquote type="cite" cite="mid:YQBPR0101MB08023741F49CB22E87A37E5EAF7E0@YQBPR0101MB0802.CANPRD01.PROD.OUTLOOK.COM">
<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="Signature">
<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="" moz-do-not-send="true">https://hustmphrrr.github.io/</a></b></font><br>
<font style="font-size:12pt" size="3"><span style="color:
rgb(69, 129, 142);"><span style="font-family:trebuchet
ms,sans-serif"></span></span></font></div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>