Skip to content

Change definition of dist_later for compatability with Transfinite Iris

Michael Sammler requested to merge msammler/new_contractive into master

This MR is one of the steps towards making Iris compatible with transfinite Iris (see simonspies/iris-parametric-index#1) by changing the definition of Contractive to be compatible with transfinite Iris. This MR tries to be forward compatible with the eventual goal of parameterizing Iris by the stepindex type. As a consequence, it already generalizes dist_S to dist_mono and introduces a stepindex tactic for solving stepindexing related goals. To simplify backwards compatibility, this MR defines the old version of dist_later as dist_later_fin and one can replace where convenient occurrences of dist_later with dist_later_fin in projects using Iris. Please let me know what you think of these changes and whether it makes more sense to factor this differently.

Downstream MRs:

Edited by Michael Sammler

Merge request reports