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.

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?

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: Sep 28 2023 at 10:01 UTC