[Agda] copattern split in Emacs?

[James Wood]

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/20191105/c1c9dd78/attachment.html>