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

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Thu Aug 4 09:12:50 CEST 2016


Dear Iris Club,

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

Thank you,
Jeehoon

-- 
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/20160804/43652b47/attachment.html>


More information about the Iris-Club mailing list