• Robbert Krebbers's avatar
    Use bundled type classes for ghost ownership. · b07dd0b5
    Robbert Krebbers authored
    * These type classes bundle an identifier into the global CMRA with a proof
      that the identifier points to the correct CMRA. Bundling allows us to get
      rid of many arguments everywhere.
    
    * I have setup the type classes so that we no longer have to keep track of the
      global CMRA identifiers. These are implicit and resolved automatically.
    
    * For heap I am also bundling the name of the heap RA instance. There always
      should be at most one heap instance so this does not introduce ambiguities.
    
    * We now have a "maps to" notation!
    b07dd0b5
auth.v 6.14 KB