[Iris-Club] Two Monoid Questions

[Gregory Malecha]

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). So it seems like there is
potentially a tradeoff between "views-style" authoritatives and bijections
(this is probably an overly simplistic understanding). So I'm wondering
what ramifications the two choices have.

On Tue, Aug 13, 2019 at 9:28 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi,
>
> On 13.08.19 14:48, Gregory Malecha wrote:
> > Naive question: What sort of reasoning are the bijections used for that
> makes
> > this lemma so crucial?
>
> I wouldn't say it is extremely crucial (clearly the author didn't even
> need it
> as their lemma is weaker), but it seems like a shame to leave a perfectly
> reasonable lemma "on the floor".
>
> ; 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/40e3a31c/attachment-0001.html>