1. 04 Apr, 2018 1 commit
  2. 21 Mar, 2018 1 commit
  3. 19 Mar, 2018 1 commit
  4. 03 Mar, 2018 2 commits
    • Robbert Krebbers's avatar
      A type class for plainly. · 6aac0120
      Robbert Krebbers authored
      Based on an earlier MR by @jung.
    • 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.
  5. 28 Feb, 2018 1 commit