[Iris-Club] Two Monoid Questions
Ralf Jung
jung at mpi-sws.org
Fri Aug 16 14:24:53 CEST 2019
My thinking is I would define a new "view" CMRA, and make "auth" an instance of
it. So it would (have to) support step-indexing. I would define SProp, but not
need a proof-mode instance or so.
But if that's too annoying, a discrete variant would also be a start. Should be
enough for the bijection.
; Ralf
On 16.08.19 14:22, Robbert Krebbers wrote:
> On 8/16/19 2:21 PM, Ralf Jung wrote:
>> and I think we could get a decent generalization of auth
>> without a lot of SProp infrastructure.
>
> In that case I presume you would keep the old auth, and make the new version
> just for the discrete case?
--
Website: https://people.mpi-sws.org/~jung/
More information about the Iris-Club
mailing list