Tracking issue for monotone RA
This is the tracking issue for the "monotone" RA from !597 (merged). A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
- How should the RA be called?
monotoneis a very general term, it would be good to find something more specific. Currently it is called
mrawhich is short but cryptic.
principalshould then likely become
mra_principaland all lemmas be prefixed with
- Do a solid review of the API surface.