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: Jan 29 2023 at 01:02 UTC