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.
- Do we really want notation for the mono_list algebra elements? The main "pro" reasin here is that
dfracotherwise 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
dfrac? Eventually we want to move everything to
dfracbut again the concern is that (without good notation), this will make the library more annoying to use.
- Do a solid review of the API surface.