Commit 6b68b171 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add is_op_plus to make iCombine behave nicer for nat.

parent ab451b4b
......@@ -404,6 +404,10 @@ Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
IsOp a b1 b2 IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
an [⋅]. *)
Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
(* IntoAnd *)
Global Instance into_and_sep p P Q : IntoAnd p (P Q) P Q.
Supports Markdown
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