[Iris-Club] Two Monoid Questions

[Gregory Malecha]

This makes sense to me. Is there a pre-packaged way to express the views
concept in Iris?

You were mentioning that it can be annoying to have fractional permissions
and such hanging out in the authoritative piece, so I was thinking that
perhaps if you had a way to generalize equality to a predicate, then you
wouldn't need to separate out the bijection.

On Tue, Aug 13, 2019 at 12:23 PM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi,
>
> > I'm not a fan of leaving lemmas "on the floor" either, but it sounds
> like this
> > issue with bijections is a deathblow to the second proposal (unless I
> > misunderstand the conversation above).
>
> It is, but it works fine for your first proposal (with a relation), which
> indicates to me that it is the better one. ;)
> Libraries will have to work with type aliases and maybe type ascriptions
> to use
> this, but only those libraries that need more freedom than the current auth
> offers will really have to do that.  And many of our users anyway tend to
> define
> derive notions for the ownership they need, so the ascriptions will not be
> needed in many places.
>
> Kind regards,
> Ralf
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190813/aa01cd17/attachment.html>