Stream: Coq users

Topic: How to locally fix?

view this post on Zulip zeesha huq (Oct 07 2021 at 07:17):

When I unfold the definitions in lemma statement to make it simple, i get fix at the start of one definition.What does it means and how I can solve it?

view this post on Zulip Gaëtan Gilbert (Oct 07 2021 at 07:24):

it's a fixpoint https://coq.github.io/doc/master/refman/language/core/inductive.html#recursive-functions-fix

Last updated: Sep 28 2023 at 10:01 UTC