Support for lambdas :) #725
Conversation
Signed-off-by: Alessio Ferrarini <alessio.ferrarini@imdea.org>
|
This should be pretty definitive even if it's useless without the corresponding PR on LH |
There was a problem hiding this comment.
Thanks @AlecsFerra. A spot that could need more discussion are the changes to evalELam.
src/Language/Fixpoint/Solver/PLE.hs
Outdated
| -- We need to refresh it as for some reason lamdba variables | ||
| -- as reflected lambdas variables for some reason are declared | ||
| -- two times, maybe we should define a new type of identifier | ||
| -- and not reuse the etabeta ones |
There was a problem hiding this comment.
Can we have an example of what it means for a lambda variable to be reflected twice?
It looks like it would be worth investigating that, instead of changing the code here to workaround a possible bug.
There was a problem hiding this comment.
Idk why but if for example you take the SKILam and remove this branch it will complain that the variable name that is used by the lambdas is declared twice in the smt file
There was a problem hiding this comment.
Tried to reproduce this in a smaller example, but couldn't. But I think it is ok to investigate it separately.
No description provided.