zohaze (May 21 2022 at 12:01): zohaze (May 21 2022 at 12:01):I have recursive function f1 and it is working properly. I am using it in another function f2. When simplify it (unfold it) then fix appears with f1,due to which i am unable to simplify it. What its mean and how to remove it? If this is termination issue then it should appear in f1 when it is working individually.But there is no issue.
Jerome Hugues (May 23 2022 at 18:27):It is a recursive function definition, see https://coq.inria.fr/distrib/current/refman/language/core/inductive.html#recursive-functions-fix. Would `induction on some paramters work?
zohaze (May 25 2022 at 04:02):Yes, it is recursive function .But it call two more functions. Like f1(f2(f3).I am unfolding f3 then f2.Now trying to unfold f1 but fix appears with f1, therefore i am unable to simplify it further. Function is performing induction on l.I don't know ( it indicates) what is the problem with l, what step i should take to make it simple or remove fix with function.
Last updated: Apr 20 2024 at 14:01 UTC