[Agda] Interactive copattern splitting

[Ulf Norell]

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'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.

/ Ulf


On Tue, Jul 15, 2014 at 12:49 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> I created a git-branch 'splitResult' that implements copattern splitting:
>
> * New feature: Interactively split result.
>
>   Make case (C-c C-c) with no variables given tries to split on the
>   result to introduce projection patterns.  The hole needs to be of
>   record type, of course.
>
>     test : {A B : Set} (a : A) (b : B) → A × B
>     test a b = ?
>
>   Result-splitting ? will produce the new clauses:
>
>     proj₁ (test a b) = ?
>     proj₂ (test a b) = ?
>
>   If hole is of function type ending in a record type, the necessary
>   pattern variables will be introduced before the split.  Thus, the
>   same result can be obtained by starting from:
>
>     test : {A B : Set} (a : A) (b : B) → A × B
>     test = ?
>
> It has been on my todo-list for long, but Cezar's question on DTP whether
> such a feature would be available in Idris soon made me jealous enough to
> implement it now.
>
> Feedback welcome.
>
> Since this feature is release-ready, I might merge it into maint-2.4.0 for
> faster dissemination.  'master' contains also features that are not so
> stable and cannot be released from one day to the next.
>
> Opinions? Ulf?
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140715/31d0f5fe/attachment-0001.html