Upstream Contractiveness
To upstream Iris parametric into Iris master, one crucial step will be changing the definition of Contractiveness
, more specifically of dist_later
. In Iris parametric, dist_later
must be defined as dist_later n x y := ∀ m, m ≺ᵢ n → x ≡{m}≡ y
to be compatible with transfinite step-indexing.
Lambda Rust and other projects depend on the current (equivalent) definition dist_later n x y := match n with 0 => True | S n => x ≡{n}≡ y end
and its reduction behavior. Thus, to stage upstreaming Iris parametric, we pull out changing the definition of dist_later
into a separate issue. To simplify backwards compatibility, we define a version of dist_later
called dist_later_fin
with the match
and replace where convenient occurrences of dist_later
with dist_later_fin
in projects using Iris.