Tracking issue for append-only list RA
This is the tracking issue for the append-only list RA from !661 (merged). A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
Open issues
- Do we really want notation for the mono_list algebra elements? The main "pro" reason here is that
dfrac
otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation and add them on-demand. - On the logic layer, should
mono_list_auth
takeQp
ordfrac
? Eventually we want to move everything todfrac
but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at #412. - Do a solid review of the API surface.