Skip to content

Adding a constructor for reflexive transitive closures into bi's

Stdpp has support for easily constructing reflexive transitive closures using rtc of https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v .

It seems fruitful to have a similar library for functions into bi.

Merge request reports