diff options
Diffstat (limited to 'theories/MSets/MSetAVL.v')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index c41df7c2..96580749 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -82,9 +82,9 @@ Definition empty := Leaf. Definition is_empty s := match s with Leaf => true | _ => false end. -(** ** Appartness *) +(** ** Membership *) -(** The [mem] function is deciding appartness. It exploits the +(** The [mem] function is deciding membership. It exploits the binary search tree invariant to achieve logarithmic complexity. *) Fixpoint mem x s := @@ -792,7 +792,7 @@ Proof. split; auto. try discriminate. intro H; elim (H x); auto. Qed. -(** * Appartness *) +(** * Membership *) Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s. Proof. |