[Iris-Club] pre-wp's definition: s, s1, and s2

Ralf Jung jung at mpi-sws.org
Thu Aug 18 13:27:07 CEST 2016

Hi Jeehoon,

> - I think in the definition of `pre-wp` (page 17, The Iris 2.0
> documentation), `s` in the 4th line is used without binding.
> - I wonder if what is the relationship between `s`, `s1`, and `s2`.. 
> More specifically, I guess `s1` and `s2` are less constrained than
> intended.  Should they be related to `s`?

Right, that `s` should have been `s1 * s2`.  This also appropriately
constrains s1 and s2. I uploaded a fixed version.

Kind regards,

More information about the Iris-Club mailing list