This MR is tackling one of the steps (simonspies/iris-parametric-index#2) towards making Iris compatible with Transfinite Iris.
It parameterizes the algebra folder by a "stepindex type"
SI. This requires according generalizations of the notions of OFEs and COFEs.
A finite stepindex type instance for
nat is provided. For this special case, we can re-derive the previous notions of OFEs and COFEs.
The rest of the development, in particular
base_logic, and everything which builds on top of these, fixes the stepindex type to
This MR is work in progress. At least the following things need to be done:
- add more comments explaining the central definitions and the rationale
- a few rewrites with
left_idare now failing and need more specific specialization for the correct instances to be found. We should try to fix this.