Skip to content

parameterize the algebra folder by the stepindex type for integration with Transfinite Iris

Lennard Gäher requested to merge simonspies/iris-parametric-index:parametric-algebra into master

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 bi, base_logic, and everything which builds on top of these, fixes the stepindex type to nat.

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_id are now failing and need more specific specialization for the correct instances to be found. We should try to fix this.

Merge request reports