<div dir="ltr">I want to release 2.4.2 before ICFP so if you can wait that long to get it into a stable release it can go in master. Since it isn&#39;t really a bug fix that makes more sense, but if you really want it out there feel free to merge it into maint and release 2.4.0.2.<div>

<br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jul 15, 2014 at 12:49 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I created a git-branch &#39;splitResult&#39; that implements copattern splitting:<br>
<br>
* New feature: Interactively split result.<br>
<br>
  Make case (C-c C-c) with no variables given tries to split on the<br>
  result to introduce projection patterns.  The hole needs to be of<br>
  record type, of course.<br>
<br>
    test : {A B : Set} (a : A) (b : B) → A × B<br>
    test a b = ?<br>
<br>
  Result-splitting ? will produce the new clauses:<br>
<br>
    proj₁ (test a b) = ?<br>
    proj₂ (test a b) = ?<br>
<br>
  If hole is of function type ending in a record type, the necessary<br>
  pattern variables will be introduced before the split.  Thus, the<br>
  same result can be obtained by starting from:<br>
<br>
    test : {A B : Set} (a : A) (b : B) → A × B<br>
    test = ?<br>
<br>
It has been on my todo-list for long, but Cezar&#39;s question on DTP whether such a feature would be available in Idris soon made me jealous enough to implement it now.<br>
<br>
Feedback welcome.<br>
<br>
Since this feature is release-ready, I might merge it into maint-2.4.0 for faster dissemination.  &#39;master&#39; contains also features that are not so stable and cannot be released from one day to the next.<br>
<br>
Opinions? Ulf?<br>
<br>
Cheers,<br>
Andreas<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>