WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris
This merge request is a first step towards generalising Iris such that large parts of its definition can be shared with Transfinite Iris. This merge request changes the definition of dist_later
such that it generalizes beyond natural numbers.
Specifically, the original definition:
dist_later n x y := match n with 0 => True | S n => x ≡{n}≡ y end
is replaced with the equivalent definition:
dist_later n x y := ∀ m, m < n → x ≡{m}≡ y
The change should be mostly local to the model of Iris with the exception of f_contractive
and solve_contractive
which are used throughout Iris (and beyond). The merge request provides alternative implementations which can handle the new definition of dist_later
.