when simplify the function then fix appears with function name , zero get added with l:list nat and some variable like torqs. What does its mean and how I can remove it?
count_occ Nat.eq_dec
(4:: (fix recycle' (a b c torqs0 : nat)
(l0 : list nat) {struct cks} :
list nat :=
match cks with
| 0 =>
if b <? torqs0
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: Jan 29 2023 at 05:03 UTC