[Iris-Club] Why a CMRA unit should be discrete?

Robbert Krebbers mail at robbertkrebbers.nl
Sat Aug 20 21:41:28 CEST 2016


Hi Jeehoon,

thanks for spotting: this requirement is no longer necessary. I have 
removed it:

  https://gitlab.mpi-sws.org/FP/iris-coq/commit/7975f872

Best,

Robbert

On 08/20/2016 05:05 PM, Jeehoon Kang wrote:
> Dear Iris Club,
>
> In the Iris 2.0 documentation's Definition 11, the 3rd condition says a
> unit should be a discrete COFE element
> (http://plv.mpi-sws.org/iris/appendix-2.0.pdf).  But I cannot see the
> intuition behind this requirement..  May I ask what is the intuition?
>
> Kind regards,
> 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>
>
>




More information about the Iris-Club mailing list