zohaze (May 21 2022 at 12:01): zohaze (May 21 2022 at 12:01):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?
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: Jan 29 2023 at 05:03 UTC