Resolved Silver issue #586

[dewert99]

Fixes #586

[alexanderjsummers]

This looks good to me - indeed, let expressions should be treated analogously to quantified variables (inside wands).

Minor but could you add to the test a case that is supposed to fail (with appropriate test annotations)? Maybe mixing two lets/quantifiers in different orders, but renaming them so that syntactically the inner assertions look identical?

[dewert99]

I've fixed the 'x' vs 'y' issue, and added an intentionally failing test.
I didn't give a test that mixes let and forall because

method test3(xs: Set[Bool]) {
  package (forall b1: Bool :: let ys == (xs) in (b1 in ys ==> true)) --* true
}

Gives java.lang.RuntimeException: Internal Error: variable ys is not defined. independently of the changes made here which should probably be it's own issue
Edit: The error is only in Carbon

[alexanderjsummers]

This looks good to me, thanks!

Please do file a Carbon issue for the crash you found when mixing binders.