Change definition of dist_later for compatability with Transfinite Iris
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:
- LambdaRust: lambda-rust!28 (merged)
- Iris Examples: no changes necessary
- Actris: actris!28 (closed)
- Simuliris: no changes necessary
- Iron: no changes necessary