Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Published 20 hours ago • verified publisher icon mattam82

Subsume funind

Open Alizter opened this issue 3 years ago • 1 comments

At the WG in Sophia we discussed that currently today coq-equations doesn't fully subsume funind so cannot be considered a full replacement for it. What does funind do that equations caan't? Let's record the details here since I've already forgotten from last week.

cc @mattam82 @ppedrot @ybertot

Alizter avatar Jun 24 '22 16:06 Alizter

https://github.com/ybertot/breadth_first_search/tree/Equations_pb

gives an example of usage of Equations that does not terminate gracefully. After a while, the Coq process simply dies, without an error message or an explanation.

Also, I don't understand why the exist constructor has to be prefixed with an @.

ybertot avatar Mar 21 '23 08:03 ybertot