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

[Jeehoon Kang]

Thank you for the clarification!

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?

Best,
Jeehoon

2016-08-18 20:27 GMT+09:00 Ralf Jung <jung at mpi-sws.org>:

> 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,
> Ralf
>
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>



-- 
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/20160819/d3c8d316/attachment.html>