Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2023-03-07T14:58:46Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/820Dune build files2023-03-07T14:58:46ZPaolo G. GiarrussoDune build filesRequires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.Requires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/710WIP: Define more uPred connectives in siProp2021-11-30T16:42:32ZHai DangWIP: Define more uPred connectives in siPropThis is an experiment initially with the step 1 + 3 of #420. Then I have experimented more with 5 and 8.This is an experiment initially with the step 1 + 3 of #420. Then I have experimented more with 5 and 8.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/616WIP: Changing the definition of contractiveness to be compatible with Transfi...2021-11-30T15:52:26ZSimon SpiesWIP: Changing the definition of contractiveness to be compatible with Transfinite IrisThis 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 n...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`.