Skip to content

GitLab

Commit 414b7b1e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Another form of associativity for `opM`.

parent 6cb0f4d2
Pipeline #5640 passed with stages
      in 6 minutes and 4 seconds
      Hide whitespace changes
      Inline Side-by-side
      Showing with 3 additions and 0 deletions
      theories/algebra/cmra.v
      View file @ 414b7b1e
      ......@@ -1333,6 +1333,9 @@ Section option.
      Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
      Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
      Lemma cmra_opM_assoc' x my mz : x ⋅? my ⋅? mz ≡ x ⋅? (my ⋅ mz).
      Proof. destruct my, mz; by rewrite /= -?assoc. Qed.
      Global Instance Some_core_id (x : A) : CoreId x → CoreId (Some x).
      Proof. by constructor. Qed.
      Global Instance option_core_id (mx : option A) :
      ......
      Markdown is supported
      0% or .
      You are about to add 0 people to the discussion. Proceed with caution.
      Finish editing this message first!
      Please register or to comment