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: Jun 24 2024 at 12:02 UTC