WIP: A library for (monotone) partial bijections.
This is based pretty much entirely on code from the runST formalization. It is also used in iris-logrel. Because there are two users of this code I was advised to submit a PR.
The idea is that
-
BIJ γ L
states thatL
is a partial bijection, -
inBij γ x y
is persistent and states thatx
andy
are in a partial bijection.
For instance you would store BIJ γ L
in some invariant to share it.
I am not sure about the choice of names and would welcome suggestions.
Tagging @amintimany.