<div dir="ltr"><div>This makes sense to me. Is there a pre-packaged way to express the views concept in Iris?</div><div><br></div><div>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.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 13, 2019 at 12:23 PM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
> I'm not a fan of leaving lemmas "on the floor" either, but it sounds like this<br>
> issue with bijections is a deathblow to the second proposal (unless I<br>
> misunderstand the conversation above).<br>
<br>
It is, but it works fine for your first proposal (with a relation), which<br>
indicates to me that it is the better one. ;)<br>
Libraries will have to work with type aliases and maybe type ascriptions to use<br>
this, but only those libraries that need more freedom than the current auth<br>
offers will really have to do that.  And many of our users anyway tend to define<br>
derive notions for the ownership they need, so the ascriptions will not be<br>
needed in many places.<br>
<br>
Kind regards,<br>
Ralf<br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div>