You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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 @.
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
The text was updated successfully, but these errors were encountered: