Commit 9814fac1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix direction of `auth_auth_validN` to make it consistent with other lemmas.

For example, `auth_auth_valid`.
parent a11a5317
......@@ -20,6 +20,8 @@ With this release, we dropped support for Coq 8.9.
(`iso_cmra_mixin_restrict`) and through an isomorphism (`iso_cmra_mixin`).
* Add a `frac_agree` library which encapsulates `frac * agree A` for some OFE
`A`, and provides some useful lemmas.
* Fix direction of `auth_auth_validN` to make it consistent with similar lemmas,
e.g., `auth_auth_valid`. The direction is now `✓{n} (● a) ↔ ✓{n} a`.
**Changes in `proofmode`:**
......
......@@ -162,7 +162,7 @@ Proof.
- by intros [?[->%(inj to_agree) []]].
- naive_solver eauto using ucmra_unit_leastN.
Qed.
Lemma auth_auth_validN n a : {n} a {n} ( a).
Lemma auth_auth_validN n a : {n} ( a) {n} a.
Proof.
rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
......
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