diff options
| author | letouzey | 2008-02-28 15:22:02 +0000 |
|---|---|---|
| committer | letouzey | 2008-02-28 15:22:02 +0000 |
| commit | b8afd9fbeac384944ccfc36cb449409eb151510e (patch) | |
| tree | 4af72cbdb828c0366465d2fb3d6df318acf3d44a /theories/FSets/FMapIntMap.v | |
| parent | 1de379a613be01b03a856d10e7a74dc7b351d343 (diff) | |
cardinal is promoted to the rank of primitive member of the FMap interface
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapIntMap.v')
| -rw-r--r-- | theories/FSets/FMapIntMap.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v index 761c8d8e68..9673d667df 100644 --- a/theories/FSets/FMapIntMap.v +++ b/theories/FSets/FMapIntMap.v @@ -98,6 +98,8 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. Definition elements (m : t A) : list (N*A) := alist_of_Map _ m. + Definition cardinal (m : t A) : nat := MapCard _ m. + Definition MapsTo (x:key)(v:A)(m:t A) := find x m = Some v. Definition In (x:key)(m:t A) := exists e:A, MapsTo x e m. @@ -319,6 +321,9 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. inversion H; auto. Qed. + Lemma cardinal_1 : forall m, cardinal m = length (elements m). + Proof. exact (@MapCard_as_length _). Qed. + Definition Equal cmp m m' := (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). |