I’m new to this community site.
I hope I’m posting this in the right place, so would you be kind to warn me if I’m not?
I have written a function using
Program Fixpoint that is consuming too
much memory to check. This happens while checking the function itself, even before
the proof obligations. When I ask Coq to check the function, the Coq process consumes
all my computer’s memory and the OOM Killer kills Coq’s process before it finishes.
What are the possibles reasons that may be causing this issue?
This is happening in the middle of big project of mine and I couldn’t reproduce it in
a small scenario.