• Robbert Krebbers's avatar
    Remove RA from the hierarchy. · b936a5ca
    Robbert Krebbers authored
    Instead, we have just a construction to create a CMRA from a RA. This
    construction is also slightly generalized, it now works for RAs over any
    timeless COFE instead of just the discrete COFE.
    
    Also:
    * Put tactics and big_ops for CMRAs in a separate file.
    * Valid is now a derived notion (as the limit of validN), so it does not have
      to be defined by hand for each CMRA.
    
    Todo:
    Make the constructions DRA -> CMRA and RA -> CMRA more uniform.
    b936a5ca
agree.v 7.55 KB