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

[Jeehoon Kang]

Dear Iris Club,

- 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`?

Thank you,
Jeehoon

-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160818/dde09150/attachment.html>