with mutual recursion?
that's what it seems like in the docs
infinite trees example in paco tutorial
with is mutual recursion when used for
Fixpoints; https://coq.inria.fr/distrib/current/refman/language/core/coinductive.html?highlight=cofixpoint#co-recursive-functions-cofix describes
cofix … with as mutual guarded corecursion — and it might be the same for
Last updated: Oct 05 2023 at 02:01 UTC