From bec3724294f7d83d8c96a1e9c97df3dcdb2a0e1b Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Jan 2007 09:45:07 +0000 Subject: Ajout operation eq dans PMap et IndexedMap git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Maps.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 69690918..22d9a370 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -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. -- cgit