Commit abaf388a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of

parents 1aae01e6 4c056f5e
......@@ -55,6 +55,7 @@ algebra/upred_tactics.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.
......@@ -34,7 +34,7 @@ Proof.
(** A typeclass for whether a variable is bound in a given
context. Making this a typeclass means we can use tpeclass search
context. Making this a typeclass means we can use typeclass search
to program solving these constraints, so this becomes extensible.
Also, since typeclass search runs *after* unification, Coq has already
inferred the X for us; if we were to go for embedded proof terms ot
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