[Agda] Why mutual is deprecated?

[Ulf Norell]

That's a mistake in the documentation. There are no plans to get rid of the
mutual keyword.
Can you file an issue for (or a PR) fixing the docs?

/ Ulf

On Fri, Feb 5, 2021 at 2:24 AM Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com>
wrote:

> 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
>
>
> _______________________________________________
> 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/20210205/f75282b1/attachment.html>