[Iris-Club] Two Monoid Questions

Gregory Malecha gregory at bedrocksystems.com
Tue Aug 13 15:45:09 CEST 2019

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>

More information about the Iris-Club mailing list