[Iris-Club] A possible typo for the definition of contractive functions
jung at mpi-sws.org
Thu Aug 4 11:09:29 CEST 2016
> 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
More information about the Iris-Club