[Agda] Why mutual is deprecated?

[Jason -Zhong Sheng- Hu]

Hi all,

According to https://agda.readthedocs.io/en/v2.6.1.2/language/mutual-recursion.html, it seems the mutual keyword is deprecated. I personally find it extremely useful and intuitive. May I know what motivates this deprecation?

Thanks,
Jason Hu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210205/0fed1bcb/attachment.html>