[Agda] copattern split in Emacs?

[Jason -Zhong Sheng- Hu]

thank you. indeed that is the trick.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of James Wood <james.wood.100 at strath.ac.uk>
Sent: November 5, 2019 4:41 PM
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: Re: [Agda] copattern split in Emacs?


Hi Jason,


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.


Regards,

James


On 05/11/2019 21:14, Jason -Zhong Sheng- Hu wrote:
Hi all,

is there a key stroke for copattern split? I looked up the docs and it seems not, right?

Thanks,
Jason Hu
https://hustmphrrr.github.io/



_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto: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/20191108/3d8e0fbd/attachment.html>