From 938823007263452cd877b06865a555e1f06c1ede Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Jun 2006 11:47:25 +0000 Subject: [PATCH] some more on equalities --- helm/software/components/cic/libraryObjects.ml | 10 ++++++++++ helm/software/components/cic/libraryObjects.mli | 2 ++ 2 files changed, 12 insertions(+) diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index df653eb9a..7a4112ad5 100644 --- a/helm/software/components/cic/libraryObjects.ml +++ b/helm/software/components/cic/libraryObjects.ml @@ -82,6 +82,12 @@ let eq_URI () = let is_eq_URI uri = List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref +let is_eq_refl_URI uri = + let urieq = UriManager.strip_xpointer uri in + is_eq_URI urieq && + not (UriManager.eq urieq uri) +;; + let is_eq_ind_URI uri = List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref @@ -92,6 +98,10 @@ let is_trans_eq_URI uri = let is_sym_eq_URI uri = List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref +let eq_refl_URI ~eq:uri = + let uri = UriManager.strip_xpointer uri in + UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)") + let sym_eq_URI ~eq:uri = try let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli index 7c31bf2bf..9dfe54902 100644 --- a/helm/software/components/cic/libraryObjects.mli +++ b/helm/software/components/cic/libraryObjects.mli @@ -29,6 +29,7 @@ val reset_defaults : unit -> unit val eq_URI : unit -> UriManager.uri option val is_eq_URI : UriManager.uri -> bool +val is_eq_refl_URI : UriManager.uri -> bool val is_eq_ind_URI : UriManager.uri -> bool val is_eq_ind_r_URI : UriManager.uri -> bool val is_trans_eq_URI : UriManager.uri -> bool @@ -36,6 +37,7 @@ val is_sym_eq_URI : UriManager.uri -> bool exception NotRecognized of string;; +val eq_refl_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri val trans_eq_URI : eq:UriManager.uri -> UriManager.uri -- 2.39.2