Commit 9f597f7b authored by Ralf Jung's avatar Ralf Jung

add a (CM)RA instance for the unit type

parent d8a82b35
......@@ -296,6 +296,9 @@ Section discrete.
End discrete.
Arguments discreteRA _ {_ _ _ _ _ _}.
(** CMRA for the unit type *)
Canonical Structure unitRA : cmraT := discreteRA ().
(** Product *)
Section prod.
Context {A B : cmraT}.
......
......@@ -231,3 +231,21 @@ Ltac solve_included :=
ra_reflection.quote;
apply ra_reflection.flatten_correct, (bool_decide_unpack _);
vm_compute; apply I.
(** An RA for the unit type *)
Instance unit_valid : Valid () := λ x, True.
Instance unit_unit : Unit () := λ x, x.
Instance unit_op : Op () := λ x y, tt.
Instance unit_minus : Minus () := λ x y, tt.
Instance unit_ra : RA ().
Proof.
split; done.
Qed.
Instance unit_empty : Empty () := tt.
Instance unit_empty_ra : RAIdentity().
Proof.
split; done.
Qed.
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