transfinite step indexing?

Stream: iris-lean

[Youngju Song]

Hi team - is there some interest in integrating transfinite step indexing to iris-lean?

[Markus de Medeiros]

Definitely! There's currently nothing stopping someone from porting OFE and CMRA to use generalized step indexing the same way that Iris-Rocq does it.

[Markus de Medeiros]

It's low on my personal list of priorities but if you'd like to try porting it I'd be happy to help.

[Mario Carneiro]

I think there is an open issue about this. At the time, I said that I would wait until it was merged upstream, so as to maintain alignment with rocq iris

[Markus de Medeiros]

(the OFE and CMRA parts have been merged upstream)

[Mario Carneiro]

prev: #iris-lean > Good first issues for new contibutors? @ 💬