[Iris-Club] A possible typo for the definition of contractive functions

Ralf Jung jung at mpi-sws.org
Thu Aug 4 11:09:29 CEST 2016

Hi Jeehoon,

> The appendix (http://plv.mpi-sws.org/iris/appendix-2.0.pdf) says:
> ```
> It [a function between two COFEs] is contractive if ∀n, x ∈ T, y ∈ T.
> (∀m < n. x m= y) ⇒ f(x) n= f(x)
> ```
> But I guess the conclusion (f(x) n= f(x)) is a typo; did you mean `f(x)
> n= f(y)`?

Indeed it is, thanks -- I will upload a fixed version of the appendix

Kind regards,

More information about the Iris-Club mailing list