Abel Nieto authored
Here's one case this lemma might be useful. Suppose we want to programmatically generate namespaces for e.g. locks: ``` Definition lockN (l : loc) := nroot .@ "lock" .@ l. ``` Then to know that two such namespaces are disjoint, we need to know that the corresponding locations are distinct. For that we use the lemma here introduced. ``` Lemma ne l1 l2 v1 v2 : l1 ↦ v1 -∗ l2 ↦ v2 -∗ ⌜l1 ≠ l2⌝. Proof. iApply mapsto_mapsto_ne. (* goal ¬ ✓ 2%Qp *) by intros . Qed. ```f227f6fa
To find the state of this project's repository at the time of any of these versions, check out the tags.