diff options
| -rw-r--r-- | lib/bij.ml | 42 | ||||
| -rw-r--r-- | lib/bij.mli | 26 |
2 files changed, 0 insertions, 68 deletions
diff --git a/lib/bij.ml b/lib/bij.ml deleted file mode 100644 index 345867f34b..0000000000 --- a/lib/bij.ml +++ /dev/null @@ -1,42 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -type ('a,'b) t = { - f : ('a,'b) Gmap.t; - finv : ('b,'a) Gmap.t } - -let empty = { f = Gmap.empty; finv = Gmap.empty } - -let map b x = Gmap.find x b.f - -let pam b y = Gmap.find y b.finv - -let dom b = Gmap.dom b.f - -let rng b = Gmap.dom b.finv - -let in_dom b x = Gmap.mem x b.f - -let in_rng b y = Gmap.mem y b.finv - -let add b (x,y) = - if in_dom b x || in_rng b y then failwith "Bij.add"; - { f = Gmap.add x y b.f; - finv = Gmap.add y x b.finv } - -let remove b x = - let y = try map b x with Not_found -> failwith "Bij.remove" in - { f = Gmap.remove x b.f; finv = Gmap.remove y b.finv } - -let app f b = Gmap.iter f b.f - -let to_list b = Gmap.to_list b.f - - diff --git a/lib/bij.mli b/lib/bij.mli deleted file mode 100644 index e67db5364c..0000000000 --- a/lib/bij.mli +++ /dev/null @@ -1,26 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(* Bijections. *) - -type ('a,'b) t - -val empty : ('a,'b) t -val map : ('a,'b) t -> 'a -> 'b -val pam : ('a,'b) t -> 'b -> 'a -val dom : ('a,'b) t -> 'a list -val rng : ('a,'b) t -> 'b list -val in_dom : ('a,'b) t -> 'a -> bool -val in_rng : ('a,'b) t -> 'b -> bool -val app : ('a -> 'b -> unit) -> ('a,'b) t -> unit -val to_list : ('a,'b) t -> ('a * 'b) list - -val add : ('a,'b) t -> 'a * 'b -> ('a,'b) t -val remove : ('a,'b) t -> 'a -> ('a,'b) t |