Stream: Coq users

Topic: meaning of fix


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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