• Robbert Krebbers's avatar
    Bundle type class for embedding. · e39f72fe
    Robbert Krebbers authored
    This change is slightly more invasive than expected: in monPred we were
    using the embedding before the BI was defined. With the new setup, this
    is no longer possible, because in order to make an instance of the
    embedding, we need to know that `monPred` is a BI. As such, we define
    `emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
    prove that they are equal to a version in terms of the embedding.