Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    ce32b224
    Simplify proof of auth_local_update. · ce32b224
    Robbert Krebbers authored
    Also, use explicit unfolding lemmas for auth_valid and auth_validN.
    The `Arguments valid _ _ !_ /` hack did not really work when one
    has to deal with the valid instance of the cmra, which underneath also
    includes a `cmra_valid`. Declaring a similar Arguments for `cmra_valid`
    is a bad idea, it will also end up unfold stuff for the exclusive and
    option CMRA.
    ce32b224
    History
    Simplify proof of auth_local_update.
    Robbert Krebbers authored
    Also, use explicit unfolding lemmas for auth_valid and auth_validN.
    The `Arguments valid _ _ !_ /` hack did not really work when one
    has to deal with the valid instance of the cmra, which underneath also
    includes a `cmra_valid`. Declaring a similar Arguments for `cmra_valid`
    is a bad idea, it will also end up unfold stuff for the exclusive and
    option CMRA.