Underscore placeholder variable
Closed this issue · 1 comments
septract commented
It would be useful to be able to write _
for an existentially-quantified placeholder. Eg. in lclist-grasshopper
:
{| isList(v) * has1Lock(curr, _) * isVal(curr, cv) |}
Right now I'm declaring _
as a named variable, but this doesn't have the right semantics. E.g.
{| foo(x,_) * bar(y,_) |}
This requires the second arguments of foo and bar to be equal.
This is a relatively safe use of existential quantification (basically a 'don't-care' quantification) so it shouldn't blow up Z3 or HSF.
How hard would it be to add this, @CaptainHayashi?
MattWindsor91 commented
Duplicate of #28, I think. Will comment on there.