diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-01-03 09:45:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-01-03 09:45:07 +0000 |
commit | bec3724294f7d83d8c96a1e9c97df3dcdb2a0e1b (patch) | |
tree | afd1f026f5526e0ca87da5b41cd367473e6a599f /lib/Maps.v | |
parent | a3bc7b24d5f21b99a37a529d06707c5f0e550679 (diff) | |
download | compcert-bec3724294f7d83d8c96a1e9c97df3dcdb2a0e1b.tar.gz compcert-bec3724294f7d83d8c96a1e9c97df3dcdb2a0e1b.zip |
Ajout operation eq dans PMap et IndexedMap
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Maps.v')
-rw-r--r-- | lib/Maps.v | 10 |
1 files changed, 10 insertions, 0 deletions
@@ -801,6 +801,14 @@ Module PMap <: MAP. Definition t (A : Set) : Set := (A * PTree.t A)%type. + Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) -> + forall (a b: t A), {a = b} + {a <> b}. + Proof. + intros. + generalize (PTree.eq H). intros. + decide equality. + Qed. + Definition init (A : Set) (x : A) := (x, PTree.empty A). @@ -877,6 +885,8 @@ Module IMap(X: INDEXED_TYPE). Definition elt := X.t. Definition elt_eq := X.eq. Definition t : Set -> Set := PMap.t. + Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) -> + forall (a b: t A), {a = b} + {a <> b} := PMap.eq. Definition init (A: Set) (x: A) := PMap.init x. Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m. Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m. |