Skip to content

WIP: Documentation on Iris equalities

Paolo G. Giarrusso requested to merge Blaisorblade/iris:doc-equalities into master

This document tries to document the subtleties involved in Iris equalities. To be somewhat self-contained, it also explains a few subtleties about how Iris-on-paper maps into Iris-coq, but only as needed.

@jung took a look at an earlier version, and suggested a few more points to discuss; FWIW, the early history is in https://gist.github.com/Blaisorblade/855b5c99b3827c306433c6da4cb689c5.

Please feel free to edit directly as you see fit; and let's maybe go through high-level concerns before the details.

Merge request reports