Skip to content

add more lemmas to list RA and move it to iris-staging

Ralf Jung requested to merge ci/ralf/list-ra into master

The list RA has awkward rules for composition due to having to fill up a prefix of the list with "holes" that contain ε. It is barely used (we know of one use by @dkhalanskiyjb); if it were submitted as a new MR nowadays we'd probably just put it into staging, but not accept it into main Iris in its current form.

So this MR "demotes" the list RA to staging. It also adds the lemmas that @dkhalanskiyjb submitted in !371 (closed) (so this MR subsumes !371 (closed)).

Merge request reports