The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I have a function (say f1)  defined as a Fixpoint containing 70 lines of Coq code.

When I do Print f1, coq shows me ~4000 lines. I guess it compiles the compact 

pattern matches into simple ones. unfolding f1 in proofs at some(but not all) places causes out of memory error after waiting >20 minutes. I suspect it unfolds the fixpoint multiple times.

I think I once noticed that on unfolding, the recursive calls were fully expanded.

(At that time f1 was much simpler, but it still took minutes)

In my proofs, I only want to unfold it exactly once. Is there some way to do it.

On searching with google, I could find only http://coq.inria.fr/cocorico/UnfoldFixpointOnce

I can try it if there is no other way.

(I'm not so keen on building from sources on my windows machine to get the development libraries that it requires)

-- Abhishek