[Iris-Club] A question on the completeness condition of COFE

[Ralf Jung]

Hi Jeehoon,

> The appendix (http://plv.mpi-sws.org/iris/appendix-2.0.pdf) says a COFE
> should be copmlete:
> ```
> ∀n, c. lim(c) =n c(n + 1) (cofe-compl)
> ```
> 
> I wonder if why it is defined as above; more concretely, why not:
> ```
> ∀n, c. lim(c) =n c(n) (cofe-compl)
> ```
> 
> Note that the above conditions are derivable from each other by (1) the
> condition of a chain that c(n) =n c(n+1); and (2) and (=n) is an
> equivalence relation.

This is simply a bug in the appendix. ;)
In Coq, the condition is

    mixin_conv_compl n c : compl c ≡{n}≡ c n

but I guess I forgot to update all parts of the appendix when I made
that change.  Thanks for pointing this out!

Kind regards,
Ralf