coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] getting rid of fix

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] getting rid of fix
Date: Thu, 10 Sep 2015 15:44:30 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-pa0-f43.google.com
Ironport-phdr: 9a23:wmy/8B188A1HgswHsmDT+DRfVm0co7zxezQtwd8ZsegVK/ad9pjvdHbS+e9qxAeQG96Lt7Qd1KGM6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZ3onLrqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDWG6noZGlcflhtWCkCR8gPzWpbvuwPxs/c71SWHa56lBYsoUCivuv84ACTjjz0KYmY0

I have a fixpoint definition which at some point unwrapped to something like
this:

fix z (x:A) := …

after some rewriting of the body it is no longer recursive. How can I get rid
of ‘fix'
and perhaps turn it into regular lambda?

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] getting rid of fix, Vadim Zaliva, 09/11/2015
- Re: [Coq-Club] getting rid of fix, Robbert Krebbers, 09/11/2015
  - Re: [Coq-Club] getting rid of fix, Vadim Zaliva, 09/11/2015
    - Re: [Coq-Club] getting rid of fix, Gregory Malecha, 09/11/2015