[Iris-Club] pre-wp's definition: s, s1, and s2
jeehoon.kang at sf.snu.ac.kr
Fri Aug 19 14:02:08 CEST 2016
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
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,
> 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...
More information about the Iris-Club