Stream: Coq users

Topic: `CoFixpoint`, `with`

view this post on Zulip Quinn (Nov 06 2021 at 12:52):

hi! is with mutual recursion?

view this post on Zulip Quinn (Nov 06 2021 at 12:52):

that's what it seems like in the docs

view this post on Zulip Quinn (Nov 06 2021 at 12:53):

infinite trees example in paco tutorial

view this post on Zulip Paolo Giarrusso (Nov 06 2021 at 14:37):

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 CoFixpoint…with (unsure)

Last updated: Oct 13 2024 at 01:02 UTC