<div dir="ltr">Thank you for the clarification!<div><br></div><div>But I am still confused of the definition of `pre-wp`..  In the 2nd line, `s` should have the type ∆(Val), mandated by `ϕ(s)`; and yet at the same time `s` should have the type Res, from `s · rf`.  May I ask if what am I missing here?</div><div><br></div><div>Best,</div><div>Jeehoon</div></div><div class="gmail_extra"><br><div class="gmail_quote">2016-08-18 20:27 GMT+09:00 Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Jeehoon,<br>
<span class=""><br>
> - I think in the definition of `pre-wp` (page 17, The Iris 2.0<br>
> documentation), `s` in the 4th line is used without binding.<br>
><br>
> - I wonder if what is the relationship between `s`, `s1`, and `s2`..<br>
> More specifically, I guess `s1` and `s2` are less constrained than<br>
> intended.  Should they be related to `s`?<br>
<br>
</span>Right, that `s` should have been `s1 * s2`.  This also appropriately<br>
constrains s1 and s2. I uploaded a fixed version.<br>
<br>
Kind regards,<br>
Ralf<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/<wbr>listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org">iris-club-unsubscribe@lists.<wbr>mpi-sws.org</a><br>
</font></span></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div>