Commit cdb38447 authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Counting CMRA" because it is already in cmra.v (called natR).

This reverts commit 4c056f5e.
parent abaf388a
Pipeline #1684 passed with stage
......@@ -55,7 +55,6 @@ algebra/upred_tactics.v
algebra/upred_big_op.v
algebra/upred_hlist.v
algebra/frac.v
algebra/count.v
algebra/csum.v
algebra/list.v
algebra/updates.v
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Notation count := nat (only parsing).
Section count.
Canonical Structure countC := leibnizC count.
Instance count_valid : Valid count := λ _, True.
Instance count_pcore : PCore count := λ _, None.
Instance count_op : Op count := λ x y, (x + y)%nat.
Definition count_ra_mixin : RAMixin nat.
Proof. by split; try apply _. Qed.
Canonical Structure countR := discreteR count count_ra_mixin.
End count.
(** Internalized properties *)
Lemma count_equivI {M} (x y : count) : x y ⊣⊢ (x = y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma count_validI {M} (x : count) : x ⊣⊢ (True : uPred M).
Proof. by uPred.unseal. 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