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

Ralf Jung jung at mpi-sws.org
Fri Aug 19 14:14:41 CEST 2016


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

Right, that should have been ϕ(v)(s). Then things hopefully make sense...

Kind regards,

More information about the Iris-Club mailing list