Skip to content

WIP: A library for (monotone) partial bijections.

Dan Frumin requested to merge dfrumin/iris-coq:bij into master

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 that L is a partial bijection,
  • inBij γ x y is persistent and states that x and y 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.

Merge request reports