• Tej Chajed's avatar
    Implement monotone partial bijections as a view · 25abf0a2
    Tej Chajed authored
    This is an alternative to !91, which was written prior to views. Using
    the view CMRA we factor the implementation into purely algebraic library
    and a logic-level wrapper. The logic-level wrapper exports resources
    which seal away the underlying ownership and has theorems which handle
    the ownership reasoning.