Skip to content

GitLab

Open
Created by Ralf Jung@jungOwner

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 called mra which is short but cryptic. principal should then likely become mra_principal and all lemmas be prefixed with mra as well.
  • Do a solid review of the API surface.

Cc @amintimany @robbertkrebbers