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.
Open issues
- How should the RA be called?
monotone
is a very general term, it would be good to find something more specific. Currently it is calledmra
which is short but cryptic.principal
should then likely becomemra_principal
and all lemmas be prefixed withmra
as well. - Do a solid review of the API surface.